hom_ext — Mathlib

English

A morphism from the total complex is uniquely determined by its composites with all inclusions ιTotal.

Русский

Морфизма из суммарного комплекса вполне достаточно определить по его композициям с инклюзиями ιTotal.

LaTeX

$$$\\forall f,g : (K.total c_{12}).X i_{12} \\to A, \\; (\\forall i_1,i_2, hi,\\; ιTotal i_1 i_2 i_{12} hi \\circ f = ιTotal i_1 i_2 i_{12} hi \\circ g) \\Rightarrow f=g$$$

Lean4

@[ext]
theorem hom_ext {A : C} {i₁₂ : I₁₂} {f g : (K.total c₁₂).X i₁₂ ⟶ A}
    (h :
      ∀ (i₁ : I₁) (i₂ : I₂) (hi : ComplexShape.π c₁ c₂ c₁₂ (i₁, i₂) = i₁₂),
        K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ f = K.ιTotal c₁₂ i₁ i₂ i₁₂ hi ≫ g) :
    f = g := by
  apply GradedObject.mapObj_ext
  rintro ⟨i₁, i₂⟩ hi
  exact h i₁ i₂ hi

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