English
The hom component respects addition: (α+β).hom = α.hom + β.hom.
Русский
Гом-компонента равна сумме гом-компонент: (α+β).hom = α.hom + β.hom.
LaTeX
$$$ (\\alpha+\\beta).hom = \\alpha.hom + \\beta.hom $$$
Lean4
@[simp]
theorem add_hom (α β : Ext X Y n) : (α + β).hom = α.hom + β.hom :=
by
let α' : Ext (X ⊞ X) Y n := (mk₀ biprod.fst).comp α (zero_add n)
let β' : Ext (X ⊞ X) Y n := (mk₀ biprod.snd).comp β (zero_add n)
have eq₁ : α + β = (mk₀ (biprod.lift (𝟙 X) (𝟙 X))).comp (α' + β') (zero_add n) := by simp [α', β']
have eq₂ : α' + β' = homEquiv.symm (α'.hom + β'.hom) :=
by
apply biprod_ext
all_goals ext; simp [α', β', ← Functor.map_comp]
simp only [eq₁, eq₂, comp_hom, Equiv.apply_symm_apply, ShiftedHom.comp_add]
congr
· dsimp [α']
rw [comp_hom, mk₀_hom, mk₀_hom]
dsimp
rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp, biprod.lift_fst, Functor.map_id, ShiftedHom.mk₀_id_comp]
· dsimp [β']
rw [comp_hom, mk₀_hom, mk₀_hom]
dsimp
rw [ShiftedHom.mk₀_comp_mk₀_assoc, ← Functor.map_comp, biprod.lift_snd, Functor.map_id, ShiftedHom.mk₀_id_comp]
