to_double_hom_ext — Mathlib

English

Same extensional principle for double morphisms from K to double f hi.

Русский

Та же принцип экстенсиональности для двойных морфизмов из K в double f hi.

LaTeX

$$$\forall (φ φ' : K \to \text{double } f hi₀₁),\; φ.f i_0 = φ'.f i_0 ∧ φ.f i_1 = φ'.f i_1 \Rightarrow φ = φ'$$$

Lean4

@[ext]
theorem to_double_hom_ext {K : HomologicalComplex C c} {φ φ' : K ⟶ double f hi₀₁} (h₀ : φ.f i₀ = φ'.f i₀)
    (h₁ : φ.f i₁ = φ'.f i₁) : φ = φ' := by
  ext k
  by_cases h : k = i₀ ∨ k = i₁
  · obtain rfl | rfl := h <;> assumption
  · simp only [not_or] at h
    apply (isZero_double_X f hi₀₁ k h.1 h.2).eq_of_tgt

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