Theorems · Definition · commutative algebra

DividedPowerAlgebra

(R : Type u_2) →
  (M : Type u_3) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_2 u_3)

The divided power algebra of a module M is defined as the ring quotient of the polynomial ring in the variables ℕ × M by the ring relation defined by DividedPowerAlgebra.Rel. We will later show that that DividedPowerAlgebra R M has divided powers. It satisfies a weak universal property for morphisms to rings with divided powers.

Defined in

Mathlib.RingTheory.DividedPowerAlgebra.Init

Cited by

48 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule