Theorems · Definition · commutative algebra

DividedPowerAlgebra.mapEquiv

{R : Type u_2} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_5} →
            [inst_3 : AddCommMonoid N] →
              [inst_4 : Module R N] → (M ≃ₗ[R] N) → DividedPowerAlgebra R M ≃ₐ[R] DividedPowerAlgebra R N

The functoriality map between divided power algebras associated with a linear equivalence of the underlying modules. Given an R-algebra S, an S-module N and an R-linear equivalence f : M →ₗ[R] N, this is the map DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N sending dp R n m to dp S n (f m).

Defined in

Mathlib.RingTheory.DividedPowerAlgebra.Init

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModule