ext — Mathlib

English

A secondary statement about Shapiro's lemma isomorphism for a broader class of functors.

Русский

Вторая формулировка леммы Шапиро для более общего класса функционалов.

LaTeX

$$groupCohomology.coindIso A n$$

Lean4

@[ext]
theorem ext {M : ModuleCat k} {x y : (inhomogeneousChains A).X n ⟶ M}
    (h : ∀ g, ModuleCat.ofHom (lsingle g) ≫ x = ModuleCat.ofHom (lsingle g) ≫ y) : x = y :=
  ModuleCat.hom_ext <| lhom_ext' fun g => ModuleCat.hom_ext_iff.1 (h g)

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