Polarity

import Linglib.Morphology.Paradigm.Polarity · namespace Morphology

This file defines polarity, the syncretism of a form over two features in which two cells share a form exactly when they differ in both features or in neither, so that each cell's form is that of its polar opposite.

Polarity is the morphological exchange of the Somali article, whose form for one gender in one number is its form for the other gender in the other number, not the polarity of a clause. A polar form separates the values of each feature at every value of the other, and it confines both features to two values.

Main definitions

Morphology.Polar: a form over two features is polar.

Main results

Morphology.Polar.injective: a polar form separates the values of the first feature at every value of the second.
Morphology.Polar.card_le_two, Morphology.Polar.card_eq_two: polarity confines either feature to two values.

References

Corbett 1991, Gender formalized
Corbett 1998, Morphology and Agreement formalized

Declarations

A form over two features is polar when two cells share a form exactly when they differ in both features or in neither.

def Polar L40–43

{G : Type u_1} {T : Type u_2} {F : Type u_3} (f : G → T → F) :

Prop

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

Used by instDecidablePolarOfFintypeOfDecidableEq, Polar.flip, Polar.injective, Polar.card_le_two, Polar.card_eq_two

Used in Fragments/Somali/Gender, Syntax/Gender/AgreementClasses, Corbett1998, Corbett2000

L47–49

L51–52

theorem Polar.injective L54–55

{G : Type u_1} {T : Type u_2} {F : Type u_3} {f : G → T → F} (h : Polar f) (t : T) :

Function.Injective fun (x : G) => f x t

Built from

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

theorem Polar.card_le_two L57–65

{G : Type u_1} {T : Type u_2} {F : Type u_3} {f : G → T → F} [Fintype G] [Nontrivial T] (h : Polar f) :

Fintype.card G ≤ 2

Built from

theorem Polar.card_eq_two L67–69

{G : Type u_1} {T : Type u_2} {F : Type u_3} {f : G → T → F} [Fintype G] [Nontrivial G] [Nontrivial T] (h : Polar f) :

Fintype.card G = 2

Built from