hom_ext — Mathlib

English

If a local differential piece vanishes due to the shape constraints, the total d also vanishes in that component.

Русский

Если локальная составляющая дифференциала равна нулю по формулам формы, то и весь дифференциал в этом компоненте равен нулю.

LaTeX

$$$d = 0$ when shape constraints force zero$$

Lean4

theorem hom_ext {j : ι₄} {A : C₄} {f g : (mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).X j ⟶ A}
    (hfg :
      ∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
        ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ f = ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ g) :
    f = g :=
  GradedObject.mapBifunctorBifunctor₂₃MapObj_ext (ρ₂₃ := ComplexShape.ρ₂₃ c₁ c₂ c₃ c₁₂ c₂₃ c₄) hfg

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