Flypitch.Colimit develops directed colimits for the concrete types used in the completeness argument. It packages directed diagrams, their quotient colimits, and the universal maps needed later for Henkin languages and their associated syntax.

structure Flypitch.colimit.directed_type : Type (u + 1)

• carrier : Type u
• rel : self.carrier → self.carrier → Prop
• h_reflexive (x : self.carrier) : self.rel x x
• h_transitive {x y z : self.carrier} : self.rel x y → self.rel y z → self.rel x z
• h_directed (x y : self.carrier) : ∃ (z : self.carrier), self.rel x z ∧ self.rel y z

theorem Flypitch.colimit.trans {D : directed_type} {i j k : D.carrier} (h₁ : D.rel i j) (h₂ : D.rel j k) : D.rel i k

structure Flypitch.colimit.directed_diagram (D : directed_type) : Type ((max u v) + 1)

• obj : D.carrier → Type v
• mor {x y : D.carrier} : D.rel x y → self.obj x → self.obj y
• h_mor {x y z : D.carrier} {f₁ : D.rel x y} {f₂ : D.rel y z} {f₃ : D.rel x z} : self.mor f₃ = self.mor f₂ ∘ self.mor f₁

@[reducible]

def Flypitch.colimit.directed_type_of_nat : directed_type

The directed type whose objects are natural numbers ordered by ≤.

Equations

• ℕ' = { carrier := ℕ, rel := fun (x1 x2 : ℕ) => x1 ≤ x2, h_reflexive := ⋯, h_transitive := ⋯, h_directed := Flypitch.colimit.directed_type_of_nat._proof_1 }

def Flypitch.colimit.termℕ' : Lean.ParserDescr

Equations

• Flypitch.colimit.termℕ' = Lean.ParserDescr.node `Flypitch.colimit.termℕ' 1024 (Lean.ParserDescr.symbol "ℕ'")

@[simp]

theorem Flypitch.colimit.ℕ_of_ℕ'.carrier : ℕ'.carrier = ℕ

@[simp]

theorem Flypitch.colimit.le_of_ℕ'.rel : ℕ'.rel = Nat.le

def Flypitch.colimit.constant_functor (D : directed_type) (A : Type v) : directed_diagram D

Equations

• Flypitch.colimit.constant_functor D A = { obj := fun (x : D.carrier) => A, mor := fun {x y : D.carrier} (x_1 : D.rel x y) => id, h_mor := ⋯ }

def Flypitch.colimit.coproduct_of_directed_diagram {D : directed_type} (F : directed_diagram D) : Type (max u u_1)

Equations

• Flypitch.colimit.coproduct_of_directed_diagram F = ((a : D.carrier) × F.obj a)

def Flypitch.colimit.canonical_inclusion_coproduct {D : directed_type} {F : directed_diagram D} (i : D.carrier) : F.obj i → coproduct_of_directed_diagram F

Equations

• Flypitch.colimit.canonical_inclusion_coproduct i x = ⟨i, x⟩

def Flypitch.colimit.germ_relation {D : directed_type} (F : directed_diagram D) : coproduct_of_directed_diagram F → coproduct_of_directed_diagram F → Prop

Equations

• Flypitch.colimit.germ_relation F ⟨i, x_2⟩ ⟨j, y⟩ = ∃ (k : D.carrier) (z : F.obj k) (f_x : D.rel i k) (f_y : D.rel j k), F.mor f_x x_2 = z ∧ F.mor f_y y = z

theorem Flypitch.colimit.germ_equivalence {D : directed_type} (F : directed_diagram D) : Equivalence (germ_relation F)

@[implicit_reducible]

instance Flypitch.colimit.coproduct_setoid {D : directed_type} (F : directed_diagram D) : Setoid (coproduct_of_directed_diagram F)

Equations

• Flypitch.colimit.coproduct_setoid F = { r := Flypitch.colimit.germ_relation F, iseqv := ⋯ }

@[reducible, inline]

abbrev Flypitch.colimit.colimit {D : directed_type} (F : directed_diagram D) : Type (max u u_1)

Equations

• Flypitch.colimit.colimit F = Quotient (Flypitch.colimit.coproduct_setoid F)

def Flypitch.colimit.canonical_map {D : directed_type} {F : directed_diagram D} (i : D.carrier) : F.obj i → colimit F

Equations

• Flypitch.colimit.canonical_map i x = Quotient.mk'' ⟨i, x⟩

theorem Flypitch.colimit.canonical_map_inj_of_transition_maps_inj {D : directed_type} {F : directed_diagram D} (i : D.carrier) (H : ∀ {i j : D.carrier} (h : D.rel i j), Function.Injective (F.mor h)) : Function.Injective (canonical_map i)

structure Flypitch.colimit.cocone {D : directed_type} (F : directed_diagram D) : Type (max (max u u_1) (w + 1))

• vertex : Type w
• map (i : D.carrier) : F.obj i → self.vertex
• h_compat {i j : D.carrier} (h : D.rel i j) : self.map i = self.map j ∘ F.mor h

def Flypitch.colimit.cocone_of_colimit {D : directed_type} (F : directed_diagram D) : cocone F

Equations

• Flypitch.colimit.cocone_of_colimit F = { vertex := Flypitch.colimit.colimit F, map := Flypitch.colimit.canonical_map, h_compat := ⋯ }

def Flypitch.colimit.universal_map {D : directed_type} {F : directed_diagram D} {V : cocone F} : colimit F → V.vertex

Equations

• Flypitch.colimit.universal_map = Quotient.lift (fun (p : Flypitch.colimit.coproduct_of_directed_diagram F) => V.map p.fst p.snd) ⋯

@[simp]

theorem Flypitch.colimit.universal_map_property {D : directed_type} {F : directed_diagram D} {V : cocone F} (i : D.carrier) (x : F.obj i) : universal_map (canonical_map i x) = V.map i x

theorem Flypitch.colimit.universal_map_inj_of_components_inj {D : directed_type} {F : directed_diagram D} {V : cocone F} (h_inj : ∀ (i : D.carrier), Function.Injective (V.map i)) : Function.Injective universal_map

noncomputable def Flypitch.colimit.germ_rep {D : directed_type} {F : directed_diagram D} (a : colimit F) : (x : coproduct_of_directed_diagram F) ×' ⟦x⟧ = a

Equations

• Flypitch.colimit.germ_rep a = ⟨Classical.choose ⋯, ⋯⟩

@[simp]

theorem Flypitch.colimit.canonical_map_quotient {D : directed_type} {F : directed_diagram D} (a : coproduct_of_directed_diagram F) : canonical_map a.fst a.snd = Quotient.mk'' a

@[simp]

theorem Flypitch.colimit.eq_mor_of_same_fiber {D : directed_type} {F : directed_diagram D} (a b : coproduct_of_directed_diagram F) {z : colimit F} (ha : Quotient.mk'' a = z) (hb : Quotient.mk'' b = z) (h_inj : ∀ (i : D.carrier), Function.Injective (canonical_map i)) (h_rel : D.rel a.fst b.fst) : F.mor h_rel a.snd = b.snd

theorem Flypitch.colimit.eq_mor_of_same_fiber' {D : directed_type} {F : directed_diagram D} (a_fst b_fst : D.carrier) (a_snd : F.obj a_fst) (b_snd : F.obj b_fst) {z : colimit F} (ha : Quotient.mk'' ⟨a_fst, a_snd⟩ = z) (hb : Quotient.mk'' ⟨b_fst, b_snd⟩ = z) (h_inj : ∀ (i : D.carrier), Function.Injective (canonical_map i)) (h_rel : D.rel a_fst b_fst) : F.mor h_rel a_snd = b_snd

@[reducible]

def Flypitch.colimit.push_to_sum_r {F : directed_diagram ℕ'} {i : ℕ} (x : F.obj i) (j : ℕ) : F.obj (i + j)

Equations

• Flypitch.colimit.push_to_sum_r x j = F.mor ⋯ x

@[reducible]

def Flypitch.colimit.push_to_sum_l {F : directed_diagram ℕ'} {j : ℕ} (x : F.obj j) (i : ℕ) : F.obj (i + j)

Equations

• Flypitch.colimit.push_to_sum_l x i = F.mor ⋯ x

theorem Flypitch.colimit.same_fiber_as_push_to_r {F : directed_diagram ℕ'} {i : ℕ} (x : F.obj i) (j : ℕ) : canonical_map i x = canonical_map (i + j) (push_to_sum_r x j)

theorem Flypitch.colimit.same_fiber_as_push_to_l {F : directed_diagram ℕ'} {j : ℕ} (x : F.obj j) (i : ℕ) : canonical_map j x = canonical_map (i + j) (push_to_sum_l x i)