zigzag_of_eqvGen_colimitTypeRel — Mathlib

English

Let F: C ⥤ Type w and c,d ∈ Σ j, F.obj j with h: Relation.EqvGen F.ColimitTypeRel c d. Then Zigzag c.1 d.1.

Русский

Пусть F: C ⥤ Type w и c,d ∈ Σ j, F.obj j с h: EqvGen F.ColimitTypeRel c d. Тогда существует Zigzag между c.1 и d.1.

LaTeX

$$$\mathrm{Zigzag}\; c.1\; d.1$$$

Lean4

/-- Let `F` be a `Type`-valued functor. If two elements `a : F c` and `b : F d` represent the same
element of `colimit F`, then `c` and `d` are related by a `Zigzag`. -/
theorem zigzag_of_eqvGen_colimitTypeRel (F : C ⥤ Type w) (c d : Σ j, F.obj j)
    (h : Relation.EqvGen F.ColimitTypeRel c d) : Zigzag c.1 d.1 := by
  induction h with
  | rel _ _ h => exact Zigzag.of_hom <| Exists.choose h
  | refl _ => exact Zigzag.refl _
  | symm _ _ _ ih => exact zigzag_symmetric ih
  | trans _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂

Похожие утверждения