Group formation

This file defines Landman's group operators on a join-semilattice E of individuals or events. Formation up packs a plural sum into an atom, the group, and dissolution down recovers the sum ([Lan89]; [Lan00b]). The carrier is any SemilatticeSup, so the operators serve the domain of individuals and the domain of events alike; in the event domain, a symmetric verb's atomic event dissolves into the sum of its directional sub-events ([Sil12]). A model on finite sets shows the two laws consistent.

Definitions

• Plurality.GroupStructure E: up and down, with a group an atom and dissolution the inverse of formation.
• Plurality.GroupStructure.finsetModel β: the model on Finset (β ⊕ ℕ), packing a plurality into the singleton of a fresh marker indexed by its code.

Main results

• Plurality.GroupStructure.up_injective: distinct sums form distinct groups.

References

• F. Landman, Groups, I (1989)
• F. Landman, Events and plurality (2000)
• T. Siloni, Reciprocal verbs and symmetry (2012)

structure Plurality.GroupStructure (E : Type u_1) [SemilatticeSup E] : Type u_1

Landman's group structure: up packs a sum into a group atom and down recovers the sum.

• up : E → E

  Group formation.

• down : E → E

  Group dissolution.

• atom_up (x : E) : Mereology.Atom (self.up x)

  A group is an atom.

• down_up (x : E) : self.down (self.up x) = x

  Dissolution inverts formation.

theorem Plurality.GroupStructure.up_injective {E : Type u_1} [SemilatticeSup E] (G : GroupStructure E) : Function.Injective G.up

A model

Finite subsets of β ⊕ ℕ under union: the β-singletons are the ordinary atoms, and packing recruits the singleton of a fresh ℕ-marker for each plurality, so groups are atoms of the same domain.

def Plurality.GroupStructure.modelUp {β : Type u_2} [Encodable β] (x : Finset (β ⊕ ℕ)) : Finset (β ⊕ ℕ)

Group formation in the model: the singleton of the marker indexed by the plurality's code.

Equations

• Plurality.GroupStructure.modelUp x = {Sum.inr (Encodable.encode x)}

theorem Plurality.GroupStructure.modelUp_injective {β : Type u_2} [Encodable β] : Function.Injective modelUp

noncomputable def Plurality.GroupStructure.finsetModel (β : Type u_3) [DecidableEq β] [Encodable β] : GroupStructure (Finset (β ⊕ ℕ))

The finite sets of β ⊕ ℕ carry a group structure, with dissolution the left inverse of formation.

Equations

• Plurality.GroupStructure.finsetModel β = { up := Plurality.GroupStructure.modelUp, down := Function.invFun Plurality.GroupStructure.modelUp, atom_up := ⋯, down_up := ⋯ }

@[simp]

theorem Plurality.GroupStructure.finsetModel_up {β : Type u_2} [Encodable β] [DecidableEq β] (x : Finset (β ⊕ ℕ)) : (finsetModel β).up x = modelUp x