Feature actions on lattices of groups

In Harbour's calculus a feature denotes a lattice of groups, the nonempty sets of some atoms, and its values act on the lattice of its host. The groups of a set of atoms X are its nonempty subsets, mathlib's interval Finset.Ioc ∅ X. The positive value adds the feature's lattice pairwise, which is mathlib's pointwise join ⊻ of set families (Finset.sups, Harbour's ⊕); the negative value subtracts the feature lattice's maximum from every group. When one feature specification denotes a proper subset of another, Lexical Complementarity confines the larger to the difference, a set difference \. Toosarvandani reuses the calculus for animacy, where the lattice of a feature added to the lattice of a larger atom set gives the groups containing one of its atoms.

Main definitions

• Plurality.FeatureAction.ominus: the negative action of a feature.
• Plurality.FeatureAction.act: the action of a feature with a given value.
• Plurality.FeatureAction.containing: the groups containing an atom of a given set.

Main results

• Plurality.FeatureAction.Ioc_sups_Ioc, Plurality.FeatureAction.Ioc_sups_containing: along an entailment chain, adding a feature's lattice gives the groups containing one of its atoms.
• Plurality.FeatureAction.containing_subset_containing_iff: such denotations are ordered as the features' atoms are.
• Plurality.FeatureAction.mem_containing_sdiff_containing_iff: Lexical Complementarity between two such denotations.

References

• [Har16a]
• [Too23]

The actions of a feature

def Plurality.FeatureAction.ominus {α : Type u_1} [DecidableEq α] (F G : Finset (Finset α)) : Finset (Finset α)

The negative action of a feature lattice F on G subtracts the maximum of F from every element of G. The empty set may result; the host head discards it.

Equations

• Plurality.FeatureAction.ominus F G = Finset.image (fun (x : Finset α) => x \ F.sup id) G

theorem Plurality.FeatureAction.mem_ominus_iff {α : Type u_1} [DecidableEq α] {F G : Finset (Finset α)} {z : Finset α} : z ∈ ominus F G ↔ ∃ g ∈ G, g \ F.sup id = z

theorem Plurality.FeatureAction.ominus_subset {α : Type u_1} [DecidableEq α] {F G G' : Finset (Finset α)} (h : G ⊆ G') : ominus F G ⊆ ominus F G'

def Plurality.FeatureAction.act {α : Type u_1} [DecidableEq α] (sign : Bool) (F G : Finset (Finset α)) : Finset (Finset α)

act sign F G is the action of the feature lattice F on G with the value sign, positive or negative.

Equations

• Plurality.FeatureAction.act sign F G = if sign = true then F ⊻ G else Plurality.FeatureAction.ominus F G

@[simp]

theorem Plurality.FeatureAction.act_true {α : Type u_1} [DecidableEq α] (F G : Finset (Finset α)) : act true F G = F ⊻ G

@[simp]

theorem Plurality.FeatureAction.act_false {α : Type u_1} [DecidableEq α] (F G : Finset (Finset α)) : act false F G = ominus F G

Groups containing an atom

def Plurality.FeatureAction.containing {α : Type u_1} [DecidableEq α] (X Y : Finset α) : Finset (Finset α)

containing X Y is the set of groups of Y that contain an atom of X.

Equations

• Plurality.FeatureAction.containing X Y = {s ∈ Finset.Ioc ∅ Y | (s ∩ X).Nonempty}

theorem Plurality.FeatureAction.mem_containing_iff {α : Type u_1} [DecidableEq α] {X Y s : Finset α} : s ∈ containing X Y ↔ s ⊆ Y ∧ (s ∩ X).Nonempty

theorem Plurality.FeatureAction.containing_mono {α : Type u_1} [DecidableEq α] {X X' Y : Finset α} (h : X ⊆ X') : containing X Y ⊆ containing X' Y

theorem Plurality.FeatureAction.containing_subset_containing_iff {α : Type u_1} [DecidableEq α] {X X' Y : Finset α} (h : X ⊆ Y) : containing X Y ⊆ containing X' Y ↔ X ⊆ X'

For X ⊆ Y, the groups of Y containing an atom of X lie among those containing an atom of X' exactly when X ⊆ X'.

theorem Plurality.FeatureAction.Ioc_sups_Ioc {α : Type u_1} [DecidableEq α] {X Y : Finset α} (h : X ⊆ Y) : Finset.Ioc ∅ X ⊻ Finset.Ioc ∅ Y = containing X Y

Adding the lattice of X to the lattice of Y ⊇ X gives the groups of Y containing an atom of X.

theorem Plurality.FeatureAction.Ioc_sups_containing {α : Type u_1} [DecidableEq α] {X Y Z : Finset α} (hXY : X ⊆ Y) (hYZ : Y ⊆ Z) : Finset.Ioc ∅ X ⊻ containing Y Z = containing X Z

Along an entailment chain X ⊆ Y ⊆ Z, adding the lattice of X to the groups of Z containing a Y-atom gives the groups containing an X-atom.

theorem Plurality.FeatureAction.mem_containing_sdiff_containing_iff {α : Type u_1} [DecidableEq α] {X Y Z s : Finset α} : s ∈ containing Y Z \ containing X Z ↔ s ⊆ Z ∧ (s ∩ Y).Nonempty ∧ ¬(s ∩ X).Nonempty

Lexical Complementarity against a more specified sibling leaves the groups containing a Y-atom but no X-atom.

theorem Plurality.FeatureAction.containing_not_subset_of_disjoint {α : Type u_1} [DecidableEq α] {X Y Z : Finset α} (hd : Disjoint X Y) (hX : X.Nonempty) (hXZ : X ⊆ Z) : ¬containing X Z ⊆ containing Y Z

Disjoint atom sets give incomparable denotations, neither more specified than the other.