shortComplexH0 — Mathlib

English

The short complex A.ρ.invariants → A → (G → A) is exact (i.e., im(i) = ker(d01)).

Русский

Короткий комплекс A.ρ.invariants → A → (G → A) точен (образ включения равно ядру d01).

LaTeX

$$The short complex with map i: A^{\\rho} → A and d01 is exact, i.e., \\operatorname{im}(i) = \\ker(d_{01} A).$$

Lean4

/-- The (exact) short complex `A.ρ.invariants ⟶ A ⟶ (G → A)`. -/
@[simps! -isSimp f g]
def shortComplexH0 : ShortComplex (ModuleCat k) :=
  mk _ _ (subtype_comp_d₀₁ A)

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