ext_succ — Mathlib

English

Alternative extensionality form for succ: equality of app' and map' components implies equality of arrows.

Русский

Альтернативная форма экстенциональности для succ: равенство компонентов app' и map' даёт равенство стрел.

LaTeX

$$$$ \\text{ext_succ}_1: (f = g) \\Leftarrow (f.app'0 = g.app'0) \\land (δ_0\\text{-map } f = δ_0\\text{-map } g) $$$$

Lean4

theorem ext_succ {F G : ComposableArrows C (n + 1)} (h₀ : F.obj' 0 = G.obj' 0) (h : F.δ₀ = G.δ₀)
    (w : F.map' 0 1 = eqToHom h₀ ≫ G.map' 0 1 ≫ eqToHom (Functor.congr_obj h.symm 0)) : F = G :=
  by
  have : ∀ i, F.obj i = G.obj i := by
    intro ⟨i, hi⟩
    rcases i with - | i
    · exact h₀
    · exact Functor.congr_obj h ⟨i, by valid⟩
  exact
    Functor.ext_of_iso
      (isoMkSucc (eqToIso h₀) (eqToIso h)
        (by
          rw [w]
          dsimp [app']
          rw [eqToHom_app, assoc, assoc, eqToHom_trans, eqToHom_refl, comp_id]))
      this (by rintro ⟨_ | _, hi⟩ <;> simp)

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