Multicoequalizer diagrams in complete lattices

We introduce the notion of bicartesian square (Lattice.BicartSq) in a lattice T. This consists of elements x₁, x₂, x₃ and x₄ such that x₂ ⊔ x₃ = x₄ and x₂ ⊓ x₃ = x₁.

It shall be shown (TODO) that if T := Set X, then the image of the associated commutative square in the category Type _ is a bicartesian square in a categorical sense (both pushout and pullback).

More generally, if T is a complete lattice, x : T, u : ι → T, v : ι → ι → T, we introduce a property MulticoequalizerDiagram x u v which says that x is the supremum of u, and that for all i and j, v i j is the minimum of u i and u j. Again, when T := Set X, we shall show (TOOD) that we obtain a multicoequalizer diagram in the category of types.

structure Lattice.BicartSq {T : Type u} (x₁ x₂ x₃ x₄ : T) [Lattice T] : Prop

A bicartesian square in a lattice consists of elements x₁, x₂, x₃ and x₄ such that x₂ ⊔ x₃ = x₄ and x₂ ⊓ x₃ = x₁.

• max_eq : x₂ ⊔ x₃ = x₄
• min_eq : x₂ ⊓ x₃ = x₁

theorem Lattice.BicartSq.le₁₂ {T : Type u} {x₁ x₂ x₃ x₄ : T} [Lattice T] (sq : BicartSq x₁ x₂ x₃ x₄) : x₁ ≤ x₂

theorem Lattice.BicartSq.le₁₃ {T : Type u} {x₁ x₂ x₃ x₄ : T} [Lattice T] (sq : BicartSq x₁ x₂ x₃ x₄) : x₁ ≤ x₃

theorem Lattice.BicartSq.le₂₄ {T : Type u} {x₁ x₂ x₃ x₄ : T} [Lattice T] (sq : BicartSq x₁ x₂ x₃ x₄) : x₂ ≤ x₄

theorem Lattice.BicartSq.le₃₄ {T : Type u} {x₁ x₂ x₃ x₄ : T} [Lattice T] (sq : BicartSq x₁ x₂ x₃ x₄) : x₃ ≤ x₄

theorem Lattice.BicartSq.commSq {T : Type u} {x₁ x₂ x₃ x₄ : T} [Lattice T] (sq : BicartSq x₁ x₂ x₃ x₄) : CategoryTheory.CommSq (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)

The commutative square associated to a bicartesian square in a lattice.

structure CompleteLattice.MulticoequalizerDiagram {T : Type u} [CompleteLattice T] {ι : Type u_1} (x : T) (u : ι → T) (v : ι → ι → T) : Prop

A multicoequalizer diagram in a complete lattice T consists of families of elements u : ι → T, v : ι → ι → T, and an element x : T such that x is the supremum of u, and for any i and j, v i j is the minimum of u i and u j.

• iSup_eq : ⨆ (i : ι), u i = x
• min_eq (i j : ι) : v i j = u i ⊓ u j

def CompleteLattice.MulticoequalizerDiagram.multispanIndex {T : Type u} [CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T} (d : MulticoequalizerDiagram x u v) : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) T

The multispan index in the category associated to the complete lattice T given by the objects u i and the minima v i j = u i ⊓ u j, when d : MulticoequalizerDiagram x u v.

Equations

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

@[simp]

theorem CompleteLattice.MulticoequalizerDiagram.multispanIndex_right {T : Type u} [CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T} (d : MulticoequalizerDiagram x u v) (a✝ : ι) : d.multispanIndex.right a✝ = u a✝

@[simp]

theorem CompleteLattice.MulticoequalizerDiagram.multispanIndex_left {T : Type u} [CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T} (d : MulticoequalizerDiagram x u v) (x✝ : (CategoryTheory.Limits.MultispanShape.prod ι).L) : d.multispanIndex.left x✝ = match x✝ with | (i, j) => v i j

@[simp]

theorem CompleteLattice.MulticoequalizerDiagram.multispanIndex_snd {T : Type u} [CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T} (d : MulticoequalizerDiagram x u v) (x✝ : (CategoryTheory.Limits.MultispanShape.prod ι).L) : d.multispanIndex.snd x✝ = CategoryTheory.homOfLE ⋯

@[simp]

theorem CompleteLattice.MulticoequalizerDiagram.multispanIndex_fst {T : Type u} [CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T} (d : MulticoequalizerDiagram x u v) (x✝ : (CategoryTheory.Limits.MultispanShape.prod ι).L) : d.multispanIndex.fst x✝ = CategoryTheory.homOfLE ⋯

def CompleteLattice.MulticoequalizerDiagram.multicofork {T : Type u} [CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T} (d : MulticoequalizerDiagram x u v) : CategoryTheory.Limits.Multicofork d.multispanIndex

The multicofork in the category associated to the complete lattice T associated to d : MulticoequalizerDiagram x u v with x : T. (In the case T := Set X, this multicofork becomes colimit after the application of the obvious functor Set X ⥤ Type _.)

Equations

• d.multicofork = CategoryTheory.Limits.Multicofork.ofπ d.multispanIndex x (fun (i : (CategoryTheory.Limits.MultispanShape.prod ι).R) => CategoryTheory.homOfLE ⋯) ⋯

@[simp]

theorem CompleteLattice.MulticoequalizerDiagram.multicofork_pt {T : Type u} [CompleteLattice T] {ι : Type u_1} {x : T} {u : ι → T} {v : ι → ι → T} (d : MulticoequalizerDiagram x u v) : d.multicofork.pt = x

theorem Lattice.BicartSq.multicoequalizerDiagram {T : Type u} [CompleteLattice T] {x₁ x₂ x₃ x₄ : T} (sq : BicartSq x₁ x₂ x₃ x₄) : CompleteLattice.MulticoequalizerDiagram x₄ (fun (i : Bool) => bif i then x₃ else x₂) fun (i j : Bool) => bif i then bif j then x₃ else x₁ else bif j then x₁ else x₂