Theorems · Definition · commutative algebra

DividedPowerAlgebra.lift

{R : Type u_2} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_4} →
            [inst_3 : CommSemiring A] →
              [inst_4 : Algebra R A] →
                {I : Ideal A} →
                  DividedPowers I → (g : M →ₗ[R] A) → (∀ (m : M), g m ∈ I) → DividedPowerAlgebra R M →ₐ[R] A

The weak universal property of a divided power algebra for morphisms to divided power rings

Defined in

Mathlib.RingTheory.DividedPowerAlgebra.Init

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCommSemiringAlgebra