Derived module algebra

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

DefinitionRoby representability#

composition with the universal law γ_d is a linear equivalence between linear maps Γ^d_R(M) → N and homogeneous polynomial laws M → N of degree d.

DividedPowerAlgebra.homogeneousLawEquiv.{u, u_1, u_2} (R : Type u) [CommSemiring R] (M : Type u_1)
  (N : Type u_2) [AddCommMonoid M] [_root_.Module R M] [AddCommMonoid N] [_root_.Module R N]
  (d : ℕ) :
  (↥(DividedPowerAlgebra.homogeneousSubmodule d) →ₗ[R] N) ≃ₗ[R]
    ↥(PolynomialLaw.homogeneousSubmodule R M N d)
Lean

Formalized in Tau Ceti as DividedPowerAlgebra.homogeneousLawEquiv.

Sources
LeanDividedPowerAlgebra.homogeneousLawEquiv
Uses 3
Statement usesDividedPowerAlgebra.gamma
Proof usesDividedPowerAlgebra.isInternal_homogeneousSubmodule · PolynomialLaw.coeff

DefinitionBase change of divided power algebras#

for a commutative R-algebra S, the canonical map S ⊗[R] Γ_R(M) → Γ_S(S ⊗[R] M) is an isomorphism of S-algebras. No flatness is assumed.

DividedPowerAlgebra.baseChangeEquiv.{u_1, u_2, u_3} (R : Type u_1) [CommSemiring R] (M : Type u_2)
  [AddCommMonoid M] [_root_.Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S] :
  TensorProduct R S (DividedPowerAlgebra R M) ≃ₐ[S] DividedPowerAlgebra S (TensorProduct R S M)
Lean

Formalized in Tau Ceti as DividedPowerAlgebra.baseChangeEquiv.

Sources
LeanDividedPowerAlgebra.baseChangeEquiv
Used by 1
Used byBase change of homogeneous divided powers

DefinitionBase change of homogeneous divided powers#

for a commutative R-algebra S, the base change isomorphism restricts to an S-linear isomorphism S ⊗[R] Γ^d_R(M) ≃ₗ[S] Γ^d_S(S ⊗[R] M) taking 1 ⊗ dp R d m to dp S d (1 ⊗ m) (baseChangeHomogeneousEquiv_one_tmul_dp). No flatness is assumed.

DividedPowerAlgebra.baseChangeHomogeneousEquiv.{u_1, u_2, u_3} (R : Type u_1) [CommSemiring R]
  (M : Type u_2) [AddCommMonoid M] [_root_.Module R M] (S : Type u_3) [CommSemiring S] [Algebra R S]
  (d : ℕ) :
  TensorProduct R S ↥(DividedPowerAlgebra.homogeneousSubmodule d) ≃ₗ[S]
    ↥(DividedPowerAlgebra.homogeneousSubmodule d)
Lean

Formalized in Tau Ceti as DividedPowerAlgebra.baseChangeHomogeneousEquiv.

Sources
LeanDividedPowerAlgebra.baseChangeHomogeneousEquiv
Uses 2
Statement usesBase change of divided power algebras
Proof usesDividedPowerAlgebra.isInternal_homogeneousSubmodule

TheoremDividedPowerAlgebra.isInternal_homogeneousSubmodule#

The homogeneous pieces of the divided power algebra form an internal direct sum: the sum map ⨁ d, Γ^d_R(M) → Γ_R(M) is bijective.

DividedPowerAlgebra.isInternal_homogeneousSubmodule.{u_1, u_2} {R : Type u_1} {M : Type u_2}
  [CommSemiring R] [AddCommMonoid M] [_root_.Module R M] :
  DirectSum.IsInternal DividedPowerAlgebra.homogeneousSubmodule
Lean

Formalized in Tau Ceti as DividedPowerAlgebra.isInternal_homogeneousSubmodule.

Sources
LeanDividedPowerAlgebra.isInternal_homogeneousSubmodule
Used by 3
Used byBase change of homogeneous divided powers · DividedPowerAlgebra.gamma · Roby representability

TheoremThe Koszul complex of a weakly regular sequence is acyclic in positive degrees#

if x = (x₀, …, xₙ₋₁) is a weakly regular sequence in R, then Hₖ₊₁(K(x)) = 0 for every k. With homologyZeroEquivSpan, the complex of finite free modules K(x) resolves R ⧸ (x₀, …, xₙ₋₁).

TauCeti.koszulComplex.exactAt_of_isWeaklyRegular.{u} {R : Type u} [CommRing R] {n : ℕ}
  (x : Fin n → R) (hx : RingTheory.Sequence.IsWeaklyRegular R (List.ofFn x)) (k : ℕ) :
  HomologicalComplex.ExactAt (TauCeti.koszulComplex (Fintype.linearCombination R x)) (k + 1)
Lean

Formalized in Tau Ceti as TauCeti.koszulComplex.exactAt_of_isWeaklyRegular.

Sources
LeanTauCeti.koszulComplex.exactAt_of_isWeaklyRegular

DefinitionZeroth Koszul homology of a finite sequence#

for x = (xᵢ) in R, the Koszul complex of the functional v ↦ ∑ᵢ vᵢ xᵢ has H₀ ≃ R ⧸ (xᵢ).

TauCeti.koszulComplex.homologyZeroEquivSpan.{u, u_1} {R : Type u} [CommRing R] {ι : Type u_1}
  [Fintype ι] (x : ι → R) :
  ↑(HomologicalComplex.homology (TauCeti.koszulComplex (Fintype.linearCombination R x)) 0) ≃ₗ[R]
    R ⧸ Ideal.span (Set.range x)
Lean

Formalized in Tau Ceti as TauCeti.koszulComplex.homologyZeroEquivSpan.

Sources
LeanTauCeti.koszulComplex.homologyZeroEquivSpan

TheoremMittag-Leffler towers have vanishing lim¹ (Stacks, Tag 07KW)# 

TauCeti.ModuleTower.subsingleton_limOne_of_isMittagLeffler.{v, u} {R : Type u} [Ring R]
  (F : TauCeti.ModuleTower R) (h : F.IsMittagLeffler) : Subsingleton F.limOne
Lean

Formalized in Tau Ceti as TauCeti.ModuleTower.subsingleton_limOne_of_isMittagLeffler.

Sources
LeanTauCeti.ModuleTower.subsingleton_limOne_of_isMittagLeffler

Definitionlim¹ of the multiplication-by-p tower is ℤ_[p] ⧸ ℤ#

lim¹ of the multiplication-by-p tower is ℤ_[p] ⧸ ℤ, the isomorphism being induced by the p-adic summation map (aₙ) ↦ ∑ₙ pⁿ aₙ (limOneMultiplicationTowerEquiv_mk).

TauCeti.ModuleTower.limOneMultiplicationTowerEquiv (p : ℕ) [Fact (Nat.Prime p)] :
  (TauCeti.ModuleTower.multiplicationTower ↑p).limOne ≃+ ℤ_[p] ⧸ (Int.castAddHom ℤ_[p]).range
Lean

Formalized in Tau Ceti as TauCeti.ModuleTower.limOneMultiplicationTowerEquiv.

Sources
LeanTauCeti.ModuleTower.limOneMultiplicationTowerEquiv

DefinitionDividedPowerAlgebra.gamma#

The universal homogeneous polynomial law γ_d : M → Γ^d_R(M) of degree d. After scalar extension to a commutative R-algebra S it sends ∑ⱼ sⱼ ⊗ mⱼ to ∑_{∑ⱼ nⱼ = d} (∏ⱼ sⱼ ^ nⱼ) ⊗ ∏ⱼ dp R nⱼ mⱼ (see gamma_toFun_sum_tmul), and its ground value is m ↦ dp R d m (see ground_gamma_apply).

DividedPowerAlgebra.gamma.{u, u_1} (R : Type u) [CommSemiring R] (M : Type u_1) [AddCommMonoid M]
  [_root_.Module R M] (d : ℕ) : M →ₚₗ[R] ↥(DividedPowerAlgebra.homogeneousSubmodule d)
Lean

Formalized in Tau Ceti as DividedPowerAlgebra.gamma.

Sources
LeanDividedPowerAlgebra.gamma
Uses 1 · Used by 1
Proof usesDividedPowerAlgebra.isInternal_homogeneousSubmodule
Used byRoby representability

DefinitionPolynomialLaw.coeff#

The coefficients of polynomial laws M →ₚₗ[R] N at the generic combination ∑ⱼ Xⱼ ⊗ mⱼ: coeff m f k is the coefficient of the monomial Xᵏ in f (∑ⱼ Xⱼ ⊗ mⱼ), computed over the polynomial ring R[Xⱼ].

PolynomialLaw.coeff.{u, u_1, u_2, u_3} (R : Type u) [CommSemiring R] {M : Type u_1} (N : Type u_2)
  [AddCommMonoid M] [_root_.Module R M] [AddCommMonoid N] [_root_.Module R N] {ι : Type u_3}
  [Fintype ι] (m : ι → M) : (M →ₚₗ[R] N) →ₗ[R] (ι →₀ ℕ) →₀ N
Lean

Formalized in Tau Ceti as PolynomialLaw.coeff.

Sources
LeanPolynomialLaw.coeff
Used by 1
Used byRoby representability

StructurePolynomialLaw.IsMultiplicative#

A polynomial law f : A →ₚₗ[R] B between R-algebras is multiplicative if f 1 = 1 and f (x * y) = f x * f y for every commutative R-algebra S and all x y : S ⊗[R] A. See IsMultiplicative.toFun_one and IsMultiplicative.toFun_mul for algebras in other universes.

PolynomialLaw.IsMultiplicative.{u, u_1, u_2} {R : Type u} [CommSemiring R] {A : Type u_1}
  {B : Type u_2} [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] (f : A →ₚₗ[R] B) : Prop
Lean

Formalized in Tau Ceti as PolynomialLaw.IsMultiplicative.

Sources
LeanPolynomialLaw.IsMultiplicative
Used by 1
Used byPolynomialLaw.algHomEquiv

DefinitionPolynomialLaw.algHomEquiv#

Algebra maps A →ₐ[R] B are identified with the multiplicative polynomial laws A →ₚₗ[R] B homogeneous of degree one, by φ ↦ φ.toLinearMap.toPolynomialLaw with inverse IsHomogeneousOfDegree.toAlgHom.

PolynomialLaw.algHomEquiv.{u, u_1, u_2} (R : Type u) [CommSemiring R] (A : Type u_1) (B : Type u_2)
  [Semiring A] [Algebra R A] [Semiring B] [Algebra R B] :
  (A →ₐ[R] B) ≃ { f // PolynomialLaw.IsHomogeneousOfDegree 1 f ∧ f.IsMultiplicative }
Lean

Formalized in Tau Ceti as PolynomialLaw.algHomEquiv.

Sources
LeanPolynomialLaw.algHomEquiv
Uses 1
Statement usesPolynomialLaw.IsMultiplicative

TheoremExistence of injective envelopes#

Every module has an injective envelope, in its own universe.

TauCeti.exists_isInjectiveEnvelope.{u, v} (R : Type u) [Ring R] (M : Type v) [AddCommGroup M]
  [_root_.Module R M] [Small.{v, u} R] : ∃ Q x x_1 i, TauCeti.IsInjectiveEnvelope i
Lean

Formalized in Tau Ceti as TauCeti.exists_isInjectiveEnvelope.

Sources
LeanTauCeti.exists_isInjectiveEnvelope

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.