hom_ext_succ — Mathlib

English

Extensionality principle for Succ level: two morphisms f,g:F ⟶ G are equal if their action on 0 and their δ₀-components agree and a compatibility holds.

Русский

Экстенциональность для уровня Succ: две morphisms равны, если их действие на 0 и δ₀-части совпадают и соблюдается совместимость.

LaTeX

$$$$ f = g \\iff [f.app 0 = g.app 0] \\land [\\delta_0\\text{-map } f = \\delta_0\\text{-map } g] $$$$

Lean4

theorem hom_ext_succ {F G : ComposableArrows C (n + 1)} {f g : F ⟶ G} (h₀ : app' f 0 = app' g 0)
    (h₁ : δ₀Functor.map f = δ₀Functor.map g) : f = g :=
  by
  ext ⟨i, hi⟩
  obtain _ | i := i
  · exact h₀
  · exact congr_app h₁ ⟨i, by valid⟩

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