Theorems · Definition · commutative algebra

DividedPowerAlgebra.map

{R : Type u_2} →
  {M : Type u_3} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (S : Type u_4) →
            [inst_3 : CommSemiring S] →
              {N : Type u_5} →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module S N] →
                      (M →ₗ[R] N) →
                        [inst_7 : Algebra R S] →
                          [IsScalarTower R S N] → DividedPowerAlgebra R M →ₐ[R] DividedPowerAlgebra S N

The functoriality map between divided power algebras associated with a linear map of the underlying modules. Given an R-algebra S, an S-module N and an R-linear map 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

12 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCommSemiringAddCommMonoidModuleModuleAlgebraIsScalarTower