comp_descToInjective — Mathlib

English

If hS is exact and J is injective, then S.g ∘ hS.descToInjective f hf = f whenever S.f ∘ f = 0.

Русский

Если hS точен и J инъективен, то S.g ∘ hS.descToInjective f hf = f при условии S.f ∘ f = 0.

LaTeX

$$$S.g \circ hS.descToInjective f hf = f$$$

Lean4

@[reassoc (attr := simp, nolint unusedHavesSuffices)]
theorem comp_descToInjective (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [Injective J] (hf : S.f ≫ f = 0) :
    S.g ≫ hS.descToInjective f hf = f := by
  dsimp [descToInjective]
  simp only [← p_fromOpcycles, assoc, Injective.comp_factorThru, p_descOpcycles]

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