hom_ext — Mathlib

English

Under the usual hypotheses of strict support, any morphism φ between two complexes is zero when they are strictly supported on the complementary sides.

Русский

При стандартных предпосылках строгой поддержки любой морфизм φ между двумя комплексами равен нулю, когда они строго поддержаны на комплементарных сторонах.

LaTeX

$$$\text{If } φ: K \to L\text{ with } [K.IsStrictlySupported e_1]\ [L.IsStrictlySupported e_2], \; φ = 0.$$$

Lean4

theorem hom_ext [K.IsStrictlySupported e₁] [L.IsStrictlySupported e₂] (φ : K ⟶ L) : φ = 0 :=
  by
  apply ac.hom_ext'
  · rw [ac.isStrictlySupportedOutside₂_iff]
    infer_instance
  · rw [ac.isStrictlySupportedOutside₁_iff]
    infer_instance

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