coinvariantsTensorObj — Mathlib

English

Tor can be computed using a projective resolution P: Tor^n(X,Y) ≅ H^n(coind X ⊗ P)_G.

Русский

Tor можно вычислить через проективную резольвенту P: Tor^n(X,Y) ≅ H^n(коинварианты X ⊗ P)_G.

LaTeX

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

Lean4

/-- Given `A : Rep k G` and a chain complex `P` in `Rep k G`, this is the chain complex whose
`n`th object is `(A ⊗ Pₙ)_G`. -/
abbrev coinvariantsTensorObj {α : Type*} [AddRightCancelSemigroup α] [One α] (A : Rep k G)
    (P : ChainComplex (Rep k G) α) : ChainComplex (ModuleCat k) α :=
  (((Rep.coinvariantsTensor k G).obj A).mapHomologicalComplex _).obj P

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