Composing modules with a ring hom

Main definitions

• Module.compHom: compose a Module with a RingHom, with action f s • m.
• RingHom.toModule: a RingHom defines a module structure by r • x = f r * x.

Tags

semimodule, module, vector space

@[reducible, inline]

abbrev Function.Surjective.moduleLeft {R : Type u_5} {S : Type u_6} {M : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul S M] (f : R →+* S) (hf : Surjective ⇑f) (hsmul : ∀ (c : R) (x : M), f c • x = c • x) : Module S M

Push forward the action of R on M along a compatible surjective map f : R →+* S.

See also Function.Surjective.mulActionLeft and Function.Surjective.distribMulActionLeft.

Equations

• Function.Surjective.moduleLeft f hf hsmul = { toDistribMulAction := Function.Surjective.distribMulActionLeft (↑f) hf hsmul, add_smul := ⋯, zero_smul := ⋯ }

@[reducible, inline]

abbrev Module.compHom {R : Type u_1} {S : Type u_2} (M : Type u_3) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] (f : S →+* R) : Module S M

Compose a Module with a RingHom, with action f s • m.

See note [reducible non-instances].

Equations

• Module.compHom M f = { toMulAction := (MulActionWithZero.compHom M f.toMonoidWithZeroHom).toMulAction, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[reducible, inline]

abbrev RingHom.toModule {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] (f : R →+* S) : Module R S

A ring homomorphism f : R →+* M defines a module structure by r • x = f r * x. See note [reducible non-instances].

Equations

• f.toModule = Module.compHom S f

def RingHom.smulOneHom {R : Type u_1} {S : Type u_2} [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] : R →+* S

If the module action of R on S is compatible with multiplication on S, then fun x ↦ x • 1 is a ring homomorphism from R to S.

This is the RingHom version of MonoidHom.smulOneHom.

When R is commutative, usually algebraMap should be preferred.

Equations

• RingHom.smulOneHom = { toMonoidHom := MonoidHom.smulOneHom, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem RingHom.smulOneHom_apply {R : Type u_1} {S : Type u_2} [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] (x : R) : smulOneHom x = x • 1

def ringHomEquivModuleIsScalarTower {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] : (R →+* S) ≃ { _inst : Module R S // IsScalarTower R S S }

A homomorphism between semirings R and S can be equivalently specified by a R-module structure on S such that S/S/R is a scalar tower.

Equations

• One or more equations did not get rendered due to their size.