torIso — Mathlib

English

For a projective resolution P of B, there is a canonical isomorphism between tor groups computed via A and B and the homology of the coinvariants object of A with respect to P.

Русский

Для проективной резольвенты P B существует канонический изоморфизм между Tor-числами, получаемыми для A и B, и гомологией косвинфертированных (коинвариантов) A по P.

LaTeX

$$torIso (A) {B} (P) (n) : ((Rep.Tor k G n).obj A).obj B ≅ (P.complex.coinvariantsTensorObj A).homology n$$

Lean4

/-- `Tor` can be computed using a projective resolution. -/
abbrev torIso (A : Rep k G) {B : Rep k G} (P : ProjectiveResolution B) (n : ℕ) :
    ((Rep.Tor k G n).obj A).obj B ≅ (P.complex.coinvariantsTensorObj A).homology n :=
  P.isoLeftDerivedObj _ n

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