Agreement classes and target genders

This file defines the agreement classes of a language's nouns and the target genders of its agreement targets, and classifies the map between the target genders of two numbers.

An agreement class is a set of nouns that take the same agreement forms on every target in every morphosyntactic form, and the controller genders of a language are its agreement classes. A target gender is a form an agreeing target distinguishes, and there may be fewer target genders than controller genders: Romanian has three of the latter over two of the former in each number. The target genders of the singular and the plural determine one another, as in French, the singular's determine the plural's without the converse, as in German, or neither determines the other, as in Romanian or Lak.

Main definitions

• Gender.agreementClasses: the kernel of the noun-level agreement map.
• Gender.targetGenders: the range of the agreement map restricted to one target.
• Gender.Parallel, Gender.Convergent, Gender.Crossed: the map between the target genders of two numbers, as each factors through the other or not.
• Gender.Polar: an exponent of two features whose polar opposites coincide.

Main results

• Gender.card_quotient_agreementClasses: the controller genders are as many as the agreement map has values.
• Gender.card_range_le_prod: the controller genders are at most the product over the targets of the target genders.
• Gender.parallel_iff_ker_eq, Gender.convergent_iff_ker_lt: the map between two numbers' target genders is the order of their kernels.
• Gender.Polar.card_le_two, Gender.Polar.parallel: polarity forces two-valued features and is a parallel system.

Implementation notes

• The index T of the agreement map is whatever the map is restricted to: a target category, a morphosyntactic form, or a pair of the two, so that target genders can be counted per target as well as per number across targets.
• Subgenders, agreement classes differing on a minority of forms, inquorate genders, small closed classes whose pattern mixes other genders, and overdifferentiated targets are the steps from agreement classes to controller genders that remain to be defined; until then the agreement classes of a fragment are its controller genders only when the fragment records no such class.

References

• [Cor91] — chapter 6
• [Zal64] — agreement classes
• [Gre63] — Universal 37: the plural never distinguishes more genders than the singular
• [Cor98] — polarity

@[reducible, inline]

abbrev Gender.agreementClasses {N : Type u_1} {T : Type u_2} {F : Type u_3} (agr : N → T → F) : Setoid N

Two nouns fall in one of Zaliznjak's agreement classes when they take the same form on every target in every morphosyntactic form.

Equations

• Gender.agreementClasses agr = Setoid.ker agr

theorem Gender.card_quotient_agreementClasses {N : Type u_1} {T : Type u_2} {F : Type u_3} (agr : N → T → F) : Nat.card (Quotient (agreementClasses agr)) = Nat.card ↑(Set.range agr)

The controller genders, being the agreement classes, are as many as the agreement map has values.

@[reducible, inline]

abbrev Gender.targetGenders {N : Type u_1} {T : Type u_2} {F : Type u_3} (agr : N → T → F) (t : T) : Set F

The target genders of a target are the forms it shows.

Equations

• Gender.targetGenders agr t = Set.range fun (x : N) => agr x t

theorem Gender.card_range_le_prod {N : Type u_1} {T : Type u_2} {F : Type u_3} [Finite N] [Fintype T] (agr : N → T → F) : Nat.card ↑(Set.range agr) ≤ ∏ t : T, Nat.card ↑(targetGenders agr t)

The controller genders are at most the product of the target genders over the targets.

theorem Gender.agreementClasses_eq_ker_of_faithful {N : Type u_1} {T : Type u_2} {F : Type u_3} {G : Type u_4} {assign : N → G} {nounAgr : N → T → F} {agr : G → T → F} (med : nounAgr = agr ∘ assign) (faith : Faithful agr) : agreementClasses nounAgr = Setoid.ker assign

When noun-level agreement is the per-gender behaviour of a faithful carrier, the agreement classes are the fibres of the assignment, so the genders are the agreement classes.

def Gender.Parallel {N : Type u_1} {F : Type u_3} {F' : Type u_4} (sg : N → F) (pl : N → F') : Prop

The map between the target genders of two numbers is parallel when each determines the other.

Equations

• Gender.Parallel sg pl = (Function.FactorsThrough pl sg ∧ Function.FactorsThrough sg pl)

def Gender.Convergent {N : Type u_1} {F : Type u_3} {F' : Type u_4} (sg : N → F) (pl : N → F') : Prop

Convergent when the first determines the second but not conversely.

Equations

• Gender.Convergent sg pl = (Function.FactorsThrough pl sg ∧ ¬Function.FactorsThrough sg pl)

def Gender.Crossed {N : Type u_1} {F : Type u_3} {F' : Type u_4} (sg : N → F) (pl : N → F') : Prop

Crossed when neither determines the other.

Equations

• Gender.Crossed sg pl = (¬Function.FactorsThrough pl sg ∧ ¬Function.FactorsThrough sg pl)

theorem Gender.parallel_iff_ker_eq {N : Type u_1} {F : Type u_3} {F' : Type u_4} {sg : N → F} {pl : N → F'} : Parallel sg pl ↔ Setoid.ker sg = Setoid.ker pl

Parallel target genders have the same kernel.

theorem Gender.convergent_iff_ker_lt {N : Type u_1} {F : Type u_3} {F' : Type u_4} {sg : N → F} {pl : N → F'} : Convergent sg pl ↔ Setoid.ker sg < Setoid.ker pl

Convergent target genders have strictly ordered kernels.

@[instance_reducible]

instance Gender.instDecidableParallel {N : Type u_1} {F : Type u_3} {F' : Type u_4} [Fintype N] [DecidableEq F] [DecidableEq F'] (sg : N → F) (pl : N → F') : Decidable (Parallel sg pl)

Equations

• Gender.instDecidableParallel sg pl = id inferInstance

@[instance_reducible]

instance Gender.instDecidableConvergent {N : Type u_1} {F : Type u_3} {F' : Type u_4} [Fintype N] [DecidableEq F] [DecidableEq F'] (sg : N → F) (pl : N → F') : Decidable (Convergent sg pl)

Equations

• Gender.instDecidableConvergent sg pl = id inferInstance

@[instance_reducible]

instance Gender.instDecidableCrossed {N : Type u_1} {F : Type u_3} {F' : Type u_4} [Fintype N] [DecidableEq F] [DecidableEq F'] (sg : N → F) (pl : N → F') : Decidable (Crossed sg pl)

Equations

• Gender.instDecidableCrossed sg pl = id inferInstance

Polarity

A fusional exponent of two features, gender and number in the Somali article, is polar when changing either value alone changes the form and changing both restores it, so that the polar opposites are identical ([Cor91] chapter 7; [Cor98]). A polar exponent is syncretic across the numbers and within neither, so it is a parallel system, and it confines both features to two values.

def Gender.Polar {T : Type u_2} {F : Type u_3} {G : Type u_4} (f : G → T → F) : Prop

An exponent of two features is polar when two cells share a form exactly when they differ in both features or in neither.

Equations

• Gender.Polar f = ∀ (g g' : G) (t t' : T), f g t = f g' t' ↔ (g = g' ↔ t = t')

@[instance_reducible]

instance Gender.instDecidablePolarOfFintypeOfDecidableEq {T : Type u_2} {F : Type u_3} {G : Type u_4} {f : G → T → F} [Fintype G] [Fintype T] [DecidableEq G] [DecidableEq T] [DecidableEq F] : Decidable (Polar f)

Equations

• Gender.instDecidablePolarOfFintypeOfDecidableEq = id inferInstance

theorem Gender.Polar.flip {T : Type u_2} {F : Type u_3} {G : Type u_4} {f : G → T → F} (h : Polar f) : Polar (_root_.flip f)

Polarity is symmetric in the two features.

theorem Gender.Polar.injective {T : Type u_2} {F : Type u_3} {G : Type u_4} {f : G → T → F} (h : Polar f) (t : T) : Function.Injective fun (x : G) => f x t

Within one value of the other feature, a polar exponent keeps every distinction.

theorem Gender.Polar.faithful {T : Type u_2} {F : Type u_3} {G : Type u_4} {f : G → T → F} [Nonempty T] (h : Polar f) : Faithful f

A polar exponent is faithful to its first feature.

theorem Gender.Polar.card_le_two {T : Type u_2} {F : Type u_3} {G : Type u_4} {f : G → T → F} [Fintype G] [Nontrivial T] (h : Polar f) : Fintype.card G ≤ 2

A polar exponent admits at most two values of either feature, since with three values of one feature two of them would share a form.

theorem Gender.Polar.card_le_two' {T : Type u_2} {F : Type u_3} {G : Type u_4} {f : G → T → F} [Fintype T] [Nontrivial G] (h : Polar f) : Fintype.card T ≤ 2

The other feature likewise.

theorem Gender.Polar.card_eq_two {T : Type u_2} {F : Type u_3} {G : Type u_4} {f : G → T → F} [Fintype G] [Nontrivial G] [Nontrivial T] (h : Polar f) : Fintype.card G = 2

Polar features are two-valued.

theorem Gender.Polar.parallel {T : Type u_2} {F : Type u_3} {G : Type u_4} {f : G → T → F} (h : Polar f) (t t' : T) : Parallel (fun (x : G) => f x t) fun (x : G) => f x t'

A polar exponent is a parallel system.