Isomorphisms of Aristotelian diagrams

Per [DKVD24] and [DS24]. An Aristotelian isomorphism is a bijection of corners preserving the labeled relation matrix; these form a groupoid — the core of the category of Aristotelian diagrams of [DKVD24]. A Boolean isomorphism ([DS24], Definition 7) is the stronger notion of a corner bijection extending to an order-isomorphism of the Boolean closures; every Boolean isomorphism is an Aristotelian one, but not conversely (the Keynes–Johnson octagons of [DS24] witness the gap).

Main declarations

• AristotelianIso — a relation-matrix-preserving corner bijection, with refl/symm/trans.
• BooleanIso, BooleanIso.toAristotelianIso — the stronger notion and the nesting.

@[simp]

theorem BooleanSubalgebra.disjoint_coe {β : Type u_1} [BooleanAlgebra β] {L : BooleanSubalgebra β} {a b : ↥L} : Disjoint ↑a ↑b ↔ Disjoint a b

Disjoint transfers across a Boolean subalgebra's coercion. UPSTREAM: belongs in Mathlib.Order.BooleanSubalgebra, cf. Complementeds.disjoint_coe.

@[simp]

theorem BooleanSubalgebra.codisjoint_coe {β : Type u_1} [BooleanAlgebra β] {L : BooleanSubalgebra β} {a b : ↥L} : Codisjoint ↑a ↑b ↔ Codisjoint a b

Codisjoint transfers across a Boolean subalgebra's coercion. UPSTREAM: belongs in Mathlib.Order.BooleanSubalgebra, cf. Complementeds.codisjoint_coe.

structure Aristotelian.AristotelianIso {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] (D : Diagram ι α) (D' : Diagram ι' α') extends ι ≃ ι' : Type (max u_1 u_2)

An Aristotelian isomorphism ([DS24], Definition 6): a corner bijection preserving and reflecting Disjoint, Codisjoint, and < — equivalently all four Aristotelian relations (map_isContradictory etc.), since these are boolean combinations.

• toFun : ι → ι'
• invFun : ι' → ι
• left_inv : Function.LeftInverse self.invFun self.toFun
• right_inv : Function.RightInverse self.invFun self.toFun
• map_disjoint (i j : ι) : Disjoint (D.φ i) (D.φ j) ↔ Disjoint (D'.φ (self.toFun i)) (D'.φ (self.toFun j))

  Joint inconsistency (⊓ = ⊥) is preserved and reflected.

• map_codisjoint (i j : ι) : Codisjoint (D.φ i) (D.φ j) ↔ Codisjoint (D'.φ (self.toFun i)) (D'.φ (self.toFun j))

  Joint exhaustiveness (⊔ = ⊤) is preserved and reflected.

• map_lt (i j : ι) : D.φ i < D.φ j ↔ D'.φ (self.toFun i) < D'.φ (self.toFun j)

  Strict entailment (subalternation) is preserved and reflected.

@[implicit_reducible]

instance Aristotelian.AristotelianIso.instEquivLike {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} : EquivLike (AristotelianIso D D') ι ι'

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Aristotelian.AristotelianIso.coe_fn_toEquiv {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} (e : AristotelianIso D D') : ⇑e.toEquiv = ⇑e

theorem Aristotelian.AristotelianIso.ext {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} {e e' : AristotelianIso D D'} (h : ∀ (i : ι), e i = e' i) : e = e'

theorem Aristotelian.AristotelianIso.ext_iff {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} {e e' : AristotelianIso D D'} : e = e' ↔ ∀ (i : ι), e i = e' i

def Aristotelian.AristotelianIso.refl {ι : Type u_1} [Fintype ι] {α : Type u_4} [BooleanAlgebra α] (D : Diagram ι α) : AristotelianIso D D

The identity Aristotelian isomorphism.

Equations

• Aristotelian.AristotelianIso.refl D = { toEquiv := Equiv.refl ι, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }

def Aristotelian.AristotelianIso.symm {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} (e : AristotelianIso D D') : AristotelianIso D' D

The inverse Aristotelian isomorphism.

Equations

• e.symm = { toEquiv := e.symm, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }

def Aristotelian.AristotelianIso.trans {ι : Type u_1} {ι' : Type u_2} {ι'' : Type u_3} [Fintype ι] [Fintype ι'] [Fintype ι''] {α : Type u_4} {α' : Type u_5} {α'' : Type u_6} [BooleanAlgebra α] [BooleanAlgebra α'] [BooleanAlgebra α''] {D : Diagram ι α} {D' : Diagram ι' α'} {D'' : Diagram ι'' α''} (e : AristotelianIso D D') (e' : AristotelianIso D' D'') : AristotelianIso D D''

Composition of Aristotelian isomorphisms.

Equations

• e.trans e' = { toEquiv := e.trans e'.toEquiv, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }

theorem Aristotelian.AristotelianIso.map_isContradictory {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} (e : AristotelianIso D D') (i j : ι) : IsContradictory (D.φ i) (D.φ j) ↔ IsContradictory (D'.φ (e i)) (D'.φ (e j))

An Aristotelian isomorphism preserves and reflects contradictoriness (Definition 6).

theorem Aristotelian.AristotelianIso.map_isContrary {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} (e : AristotelianIso D D') (i j : ι) : IsContrary (D.φ i) (D.φ j) ↔ IsContrary (D'.φ (e i)) (D'.φ (e j))

An Aristotelian isomorphism preserves and reflects contrariety (Definition 6).

theorem Aristotelian.AristotelianIso.map_isSubcontrary {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} (e : AristotelianIso D D') (i j : ι) : IsSubcontrary (D.φ i) (D.φ j) ↔ IsSubcontrary (D'.φ (e i)) (D'.φ (e j))

An Aristotelian isomorphism preserves and reflects subcontrariety (Definition 6).

theorem Aristotelian.AristotelianIso.map_isSubaltern {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} (e : AristotelianIso D D') (i j : ι) : IsSubaltern (D.φ i) (D.φ j) ↔ IsSubaltern (D'.φ (e i)) (D'.φ (e j))

An Aristotelian isomorphism preserves and reflects subalternation (Definition 6).

Boolean isomorphism (Definition 7) and the nesting

def Aristotelian.Diagram.corner {ι : Type u_1} [Fintype ι] {α : Type u_4} [BooleanAlgebra α] (D : Diagram ι α) (i : ι) : ↥(BooleanSubalgebra.closure (Set.range D.φ))

The i-th corner of a diagram, viewed inside its Boolean closure.

Equations

• D.corner i = ⟨D.φ i, ⋯⟩

@[simp]

theorem Aristotelian.Diagram.coe_corner {ι : Type u_1} [Fintype ι] {α : Type u_4} [BooleanAlgebra α] (D : Diagram ι α) (i : ι) : ↑(D.corner i) = D.φ i

structure Aristotelian.BooleanIso {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] (D : Diagram ι α) (D' : Diagram ι' α') : Type (max (max (max u_1 u_2) u_4) u_5)

A Boolean isomorphism ([DS24], Definition 7): a corner bijection that extends to an order-isomorphism of the Boolean closures.

• toEquiv : ι ≃ ι'

  The underlying corner bijection.

• closureIso : ↥(BooleanSubalgebra.closure (Set.range D.φ)) ≃o ↥(BooleanSubalgebra.closure (Set.range D'.φ))

  The order-isomorphism of Boolean closures extending it.

• extends_corners (i : ι) : self.closureIso (D.corner i) = D'.corner (self.toEquiv i)

  closureIso carries corners to corners.

theorem Aristotelian.BooleanIso.ext {ι : Type u_1} {ι' : Type u_2} {inst✝ : Fintype ι} {inst✝¹ : Fintype ι'} {α : Type u_4} {α' : Type u_5} {inst✝² : BooleanAlgebra α} {inst✝³ : BooleanAlgebra α'} {D : Diagram ι α} {D' : Diagram ι' α'} {x y : BooleanIso D D'} (toEquiv : x.toEquiv = y.toEquiv) (closureIso : x.closureIso = y.closureIso) : x = y

theorem Aristotelian.BooleanIso.ext_iff {ι : Type u_1} {ι' : Type u_2} {inst✝ : Fintype ι} {inst✝¹ : Fintype ι'} {α : Type u_4} {α' : Type u_5} {inst✝² : BooleanAlgebra α} {inst✝³ : BooleanAlgebra α'} {D : Diagram ι α} {D' : Diagram ι' α'} {x y : BooleanIso D D'} : x = y ↔ x.toEquiv = y.toEquiv ∧ x.closureIso = y.closureIso

def Aristotelian.BooleanIso.refl {ι : Type u_1} [Fintype ι] {α : Type u_4} [BooleanAlgebra α] (D : Diagram ι α) : BooleanIso D D

The identity Boolean isomorphism.

Equations

• Aristotelian.BooleanIso.refl D = { toEquiv := Equiv.refl ι, closureIso := OrderIso.refl ↥(BooleanSubalgebra.closure (Set.range D.φ)), extends_corners := ⋯ }

def Aristotelian.BooleanIso.symm {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} (e : BooleanIso D D') : BooleanIso D' D

The inverse Boolean isomorphism.

Equations

• e.symm = { toEquiv := e.toEquiv.symm, closureIso := e.closureIso.symm, extends_corners := ⋯ }

def Aristotelian.BooleanIso.trans {ι : Type u_1} {ι' : Type u_2} {ι'' : Type u_3} [Fintype ι] [Fintype ι'] [Fintype ι''] {α : Type u_4} {α' : Type u_5} {α'' : Type u_6} [BooleanAlgebra α] [BooleanAlgebra α'] [BooleanAlgebra α''] {D : Diagram ι α} {D' : Diagram ι' α'} {D'' : Diagram ι'' α''} (e : BooleanIso D D') (e' : BooleanIso D' D'') : BooleanIso D D''

Composition of Boolean isomorphisms.

Equations

• e.trans e' = { toEquiv := e.toEquiv.trans e'.toEquiv, closureIso := e.closureIso.trans e'.closureIso, extends_corners := ⋯ }

def Aristotelian.BooleanIso.toAristotelianIso {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} (bi : BooleanIso D D') : AristotelianIso D D'

Every Boolean isomorphism is an Aristotelian isomorphism ([DS24], p.13); the converse fails (the Keynes–Johnson octagons witness the gap).

Equations

• bi.toAristotelianIso = { toEquiv := bi.toEquiv, map_disjoint := ⋯, map_codisjoint := ⋯, map_lt := ⋯ }

@[implicit_reducible]

instance Aristotelian.BooleanIso.instCoeOutAristotelianIso {ι : Type u_1} {ι' : Type u_2} [Fintype ι] [Fintype ι'] {α : Type u_4} {α' : Type u_5} [BooleanAlgebra α] [BooleanAlgebra α'] {D : Diagram ι α} {D' : Diagram ι' α'} : CoeOut (BooleanIso D D') (AristotelianIso D D')

Forget a Boolean isomorphism down to its underlying Aristotelian isomorphism.

Equations

• Aristotelian.BooleanIso.instCoeOutAristotelianIso = { coe := Aristotelian.BooleanIso.toAristotelianIso }