Tor — Mathlib

English

If Y is projective, then all higher Tors vanish; the higher tor groups vanish in particular for all n.

Русский

Если Y проективно, то все высшие Tor-числа исчезают; в частности, Tor выше нуля равны нулю.

LaTeX

$$IsZero( ((Tor k G (n+1)).obj X).obj Y )$$

Lean4

/-- The left-derived functors given by deriving the second argument of `A, B ↦ (A ⊗[k] B)_G`. -/
@[simps]
def Tor (n : ℕ) : Rep k G ⥤ Rep k G ⥤ ModuleCat k
    where
  obj X := Functor.leftDerived ((coinvariantsTensor k G).obj X) n
  map f := NatTrans.leftDerived ((coinvariantsTensor k G).map f) n

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