NF weak partition development: Flypitch4.Colimit.

Lean 3 → Lean 4 Port: Notes for Colimit.lean

Scope

Only declarations needed by src/henkin.lean are ported. The following are dropped:

• constant_functor — 0 uses outside colimit.lean
• trans (the colimit lemma) — 0 uses outside colimit.lean; Trans in Lean 4 is a typeclass

Quotient API choices

• colimit is @[reducible] so that Quotient.lift, Quotient.sound, etc. can unify with it
• Lean 3 quotient.mk → Lean 4 Quotient.mk (coproduct_setoid F)
• Lean 3 quotient.lift → Lean 4 Quotient.lift
• Lean 3 quotient.eq → Lean 4 Quotient.exact / Quotient.sound

cocone_of_colimit kept as an internal helper

Used internally to prove same_fiber_as_push_to_r/l, which henkin.lean uses directly.

Structures: Reflexive / Transitive deprecated in Lean 4

Use explicit ∀ hypotheses in directed_type.

structure NFChoice.colimit.DirectedType : Type (u + 1)

Flypitch construction directed_type, retained by the first-order soundness and completeness development.

• carrier : Type u

  The carrier component of the corresponding first-order structure.

• rel : self.carrier → self.carrier → Prop

  The rel component of the corresponding first-order structure.

• 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

structure NFChoice.colimit.DirectedDiagram (D : DirectedType) : Type (max (u + 1) (v + 1))

Flypitch construction directed_diagram, retained by the first-order soundness and completeness development.

• obj : D.carrier → Type v

  The obj component of the corresponding first-order structure.

• mor {x y : D.carrier} : D.rel x y → self.obj x → self.obj y

  The mor component of the corresponding first-order structure.

• h_mor {x y z : D.carrier} {f1 : D.rel x y} {f2 : D.rel y z} {f3 : D.rel x z} : self.mor f3 = self.mor f2 ∘ self.mor f1

@[reducible]

def NFChoice.colimit.directedTypeOfNat : DirectedType

Flypitch construction directed_type_of_nat, retained by the first-order soundness and completeness development.

Equations

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

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

Notation for the corresponding first-order syntax or interpretation operation.

Equations

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

def NFChoice.colimit.coproductOfDirectedDiagram {D : DirectedType} (F : DirectedDiagram D) : Type (max u v)

Flypitch construction coproduct_of_directed_diagram, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.coproductOfDirectedDiagram F = ((a : D.carrier) × F.obj a)

def NFChoice.colimit.canonicalInclusionCoproduct {D : DirectedType} {F : DirectedDiagram D} (i : D.carrier) : F.obj i → coproductOfDirectedDiagram F

Flypitch construction canonical_inclusion_coproduct, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.canonicalInclusionCoproduct i x = ⟨i, x⟩

def NFChoice.colimit.germRelation {D : DirectedType} (F : DirectedDiagram D) : coproductOfDirectedDiagram F → coproductOfDirectedDiagram F → Prop

Flypitch construction germ_relation, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.germRelation F ⟨j, y⟩ ⟨j_1, y_1⟩ = ∃ (k : D.carrier) (z : F.obj k) (f_x : D.rel j k) (f_y : D.rel j_1 k), F.mor f_x y = z ∧ F.mor f_y y_1 = z

theorem NFChoice.colimit.germ_equivalence {D : DirectedType} (F : DirectedDiagram D) : Equivalence (germRelation F)

def NFChoice.colimit.coproductSetoid {D : DirectedType} (F : DirectedDiagram D) : Setoid (coproductOfDirectedDiagram F)

The setoid on the coproduct given by germ equivalence

Equations

• NFChoice.colimit.coproductSetoid F = { r := NFChoice.colimit.germRelation F, iseqv := ⋯ }

@[reducible]

def NFChoice.colimit.LimitCarrier {D : DirectedType} (F : DirectedDiagram D) : Type (max u v)

Flypitch construction LimitCarrier, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.LimitCarrier F = Quotient (NFChoice.colimit.coproductSetoid F)

def NFChoice.colimit.canonicalMap {D : DirectedType} {F : DirectedDiagram D} (i : D.carrier) : F.obj i → LimitCarrier F

Flypitch construction canonical_map, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.canonicalMap i x = ⟦⟨i, x⟩⟧

theorem NFChoice.colimit.canonical_map_inj_of_transition_maps_inj {D : DirectedType} {F : DirectedDiagram D} (i : D.carrier) (H : ∀ {i j : D.carrier} (h : D.rel i j), Function.Injective (F.mor h)) : Function.Injective (canonicalMap i)

structure NFChoice.colimit.cocone {D : DirectedType} (F : DirectedDiagram D) : Type (max (max (u_1 + 1) u_2) u_3)

Flypitch construction cocone, retained by the first-order soundness and completeness development.

• vertex : Type u_1

  The vertex component of the corresponding first-order structure.

• map (i : D.carrier) : F.obj i → self.vertex

  The map component of the corresponding first-order structure.

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

def NFChoice.colimit.coconeOfColimit {D : DirectedType} (F : DirectedDiagram D) : cocone F

Flypitch construction cocone_of_colimit, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.coconeOfColimit F = { vertex := NFChoice.colimit.LimitCarrier F, map := NFChoice.colimit.canonicalMap, h_compat := ⋯ }

def NFChoice.colimit.universalMap {D : DirectedType} {F : DirectedDiagram D} {V : cocone F} : LimitCarrier F → V.vertex

Flypitch construction universal_map, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.universalMap = Quotient.lift (fun (p : NFChoice.colimit.coproductOfDirectedDiagram F) => V.map p.fst p.snd) ⋯

@[simp]

theorem NFChoice.colimit.universal_map_property {D : DirectedType} {F : DirectedDiagram D} {V : cocone F} (i : D.carrier) (x : F.obj i) : universalMap (canonicalMap i x) = V.map i x

theorem NFChoice.colimit.universal_map_inj_of_components_inj {D : DirectedType} {F : DirectedDiagram D} {V : cocone F} (h_inj : ∀ (i : D.carrier), Function.Injective (V.map i)) : Function.Injective universalMap

noncomputable def NFChoice.colimit.germRep {D : DirectedType} {F : DirectedDiagram D} (a : LimitCarrier F) : (x : coproductOfDirectedDiagram F) ×' ⟦x⟧ = a

Flypitch construction germ_rep, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.germRep a = NFChoice.Classical.psigmaOfExists ⋯

@[simp]

theorem NFChoice.colimit.canonical_map_quotient {D : DirectedType} {F : DirectedDiagram D} (a : coproductOfDirectedDiagram F) : canonicalMap a.fst a.snd = ⟦a⟧

@[simp]

theorem NFChoice.colimit.eq_mor_of_same_fiber {D : DirectedType} {F : DirectedDiagram D} (a b : coproductOfDirectedDiagram F) {z : LimitCarrier F} (Ha : ⟦a⟧ = z) (Hb : ⟦b⟧ = z) (H_inj : ∀ (i : D.carrier), Function.Injective (canonicalMap i)) (H_rel : D.rel a.fst b.fst) : F.mor H_rel a.snd = b.snd

theorem NFChoice.colimit.eq_mor_of_same_fiber' {D : DirectedType} {F : DirectedDiagram D} (a_fst b_fst : D.carrier) (a_snd : F.obj a_fst) (b_snd : F.obj b_fst) {z : LimitCarrier F} (Ha : ⟦⟨a_fst, a_snd⟩⟧ = z) (Hb : ⟦⟨b_fst, b_snd⟩⟧ = z) (H_inj : ∀ (i : D.carrier), Function.Injective (canonicalMap i)) (H_rel : D.rel a_fst b_fst) : F.mor H_rel a_snd = b_snd

@[reducible]

def NFChoice.colimit.pushToSumR {F : DirectedDiagram ℕ'} {i : ℕ} (x : F.obj i) (j : ℕ) : F.obj (i + j)

Flypitch construction push_to_sum_r, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.pushToSumR x j = F.mor ⋯ x

@[reducible]

def NFChoice.colimit.pushToSumL {F : DirectedDiagram ℕ'} {j : ℕ} (x : F.obj j) (i : ℕ) : F.obj (i + j)

Flypitch construction push_to_sum_l, retained by the first-order soundness and completeness development.

Equations

• NFChoice.colimit.pushToSumL x i = F.mor ⋯ x

theorem NFChoice.colimit.same_fiber_as_push_to_r {F : DirectedDiagram ℕ'} {i : ℕ} (x : F.obj i) (j : ℕ) : canonicalMap i x = canonicalMap (i + j) (pushToSumR x j)

theorem NFChoice.colimit.same_fiber_as_push_to_l {F : DirectedDiagram ℕ'} {j : ℕ} (x : F.obj j) (i : ℕ) : canonicalMap j x = canonicalMap (i + j) (pushToSumL x i)

def NFChoice.omegaColimit.mapAux (F : ℕ → Type u_1) (h_succ : {i : ℕ} → F i → F (i + 1)) (x y : ℕ) : x ≤ y → F x → F y

Flypitch construction map_aux, retained by the first-order soundness and completeness development.

Equations

• NFChoice.omegaColimit.mapAux F h_succ x✝ 0 h = ⋯.mpr id
• NFChoice.omegaColimit.mapAux F h_succ x✝ y.succ h = if hx : x✝ = y + 1 then ⋯.mpr id else h_succ ∘ NFChoice.omegaColimit.mapAux F (fun {i : ℕ} => h_succ) x✝ y ⋯

def NFChoice.omegaColimit.diagram.mk.map {F : ℕ → Type u_1} {h_succ : {i : ℕ} → F i → F (i + 1)} (x y : ℕ) (h : x ≤ y) : F x → F y

Flypitch construction diagram.mk.map, retained by the first-order soundness and completeness development.

Equations

• NFChoice.omegaColimit.diagram.mk.map x y h = NFChoice.omegaColimit.mapAux F (fun {i : ℕ} => h_succ) x y h

@[simp]

theorem NFChoice.omegaColimit.diagram.mk.map_self_id {F : ℕ → Type u_1} {h_succ : (i : ℕ) → F i → F (i + 1)} (x : ℕ) : map x x ⋯ = id

theorem NFChoice.omegaColimit.diagram.mk.map_inj {F : ℕ → Type u_1} {h_succ : (i : ℕ) → F i → F (i + 1)} {h_inj : ∀ {i : ℕ}, Function.Injective (h_succ i)} (x y : ℕ) (h : x ≤ y) : Function.Injective (map x y h)

def NFChoice.omegaColimit.diagram.mk (F : ℕ → Type u_1) (h_succ : {i : ℕ} → F i → F (i + 1)) : colimit.DirectedDiagram ℕ'

Flypitch construction diagram.mk, retained by the first-order soundness and completeness development.

Equations

• NFChoice.omegaColimit.diagram.mk F h_succ = { obj := F, mor := fun {x y : ℕ'.carrier} (h : ℕ'.rel x y) => NFChoice.omegaColimit.diagram.mk.map x y h, h_mor := ⋯ }