Mathlib.Algebra.Module.RingHom

Module docstring

{"# 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 "}

Function.Surjective.moduleLeft abbrev

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

Full source

/-- 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`.
-/
abbrev Function.Surjective.moduleLeft {R S M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
    [Semiring S] [SMul S M] (f : R →+* S) (hf : Function.Surjective f)
    (hsmul : ∀ (c) (x : M), f c • x = c • x) : Module S M :=
  { hf.distribMulActionLeft f.toMonoidHom hsmul with
    zero_smul := fun x => by rw [← f.map_zero, hsmul, zero_smul]
    add_smul := hf.forall₂.mpr fun a b x => by simp only [← f.map_add, hsmul, add_smul] }

Module Structure Induced by a Surjective Ring Homomorphism

Informal description

Let $R$ and $S$ be semirings, and $M$ be an additive commutative monoid with a module structure over $R$. Given a surjective ring homomorphism $f : R \to S$ and a scalar multiplication operation $\bullet$ of $S$ on $M$ such that for all $c \in R$ and $x \in M$, we have $f(c) \bullet x = c \bullet x$, then $M$ can be endowed with a module structure over $S$.

Module.compHom abbrev

[Semiring S] (f : S →+* R) : Module S M

Full source

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

See note [reducible non-instances]. -/
abbrev Module.compHom [Semiring S] (f : S →+* R) : Module S M :=
  { MulActionWithZero.compHom M f.toMonoidWithZeroHom, DistribMulAction.compHom M (f : S →* R) with
    -- Porting note: the `show f (r + s) • x = f r • x + f s • x` wasn't needed in mathlib3.
    -- Somehow, now that `SMul` is heterogeneous, it can't unfold earlier fields of a definition for
    -- use in later fields.  See
    -- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Heterogeneous.20scalar.20multiplication
    -- TODO(jmc): there should be a rw-lemma `smul_comp` close to `SMulZeroClass.compFun`
    add_smul := fun r s x => show f (r + s) • x = f r • x + f s • x by simp [add_smul] }

Module structure induced by composition with a ring homomorphism

Informal description

Given a semiring $S$, a ring homomorphism $f \colon S \to R$, and a module $M$ over $R$, the composition $\mathrm{Module.compHom}$ defines a module structure on $M$ over $S$ via the scalar multiplication $s \bullet m = f(s) \bullet m$ for $s \in S$ and $m \in M$.

RingHom.toModule abbrev

[Semiring R] [Semiring S] (f : R →+* S) : Module R S

Full source

/-- A ring homomorphism `f : R →+* M` defines a module structure by `r • x = f r * x`.
See note [reducible non-instances]. -/
abbrev RingHom.toModule [Semiring R] [Semiring S] (f : R →+* S) : Module R S :=
  Module.compHom S f

Module Structure on $S$ Induced by Ring Homomorphism $f \colon R \to S$

Informal description

Given a ring homomorphism $f \colon R \to S$ between semirings $R$ and $S$, the semiring $S$ can be endowed with a module structure over $R$ where the scalar multiplication is defined by $r \bullet x = f(r) \cdot x$ for $r \in R$ and $x \in S$.

RingHom.smulOneHom definition

[Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] : R →+* S

Full source

/-- 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. -/
@[simps!] def RingHom.smulOneHom
    [Semiring R] [NonAssocSemiring S] [Module R S] [IsScalarTower R S S] : R →+* S where
  __ := MonoidHom.smulOneHom
  map_zero' := zero_smul R 1
  map_add' := (add_smul · · 1)

Ring homomorphism induced by scalar multiplication with identity

Informal description

Given a semiring $R$ and a non-associative semiring $S$ equipped with a module structure over $R$ such that the scalar multiplication is compatible with multiplication in $S$ (i.e., $[IsScalarTower\ R\ S\ S]$), the function $x \mapsto x \cdot 1_S$ defines a ring homomorphism from $R$ to $S$, where $1_S$ is the multiplicative identity of $S$.

ringHomEquivModuleIsScalarTower definition

[Semiring R] [Semiring S] : (R →+* S) ≃ { _inst : Module R S // IsScalarTower R S S }

Full source

/-- 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. -/
def ringHomEquivModuleIsScalarTower [Semiring R] [Semiring S] :
    (R →+* S) ≃ {_inst : Module R S // IsScalarTower R S S} where
  toFun f := ⟨Module.compHom S f, SMul.comp.isScalarTower _⟩
  invFun := fun ⟨_, _⟩ ↦ RingHom.smulOneHom
  left_inv f := RingHom.ext fun r ↦ mul_one (f r)
  right_inv := fun ⟨_, _⟩ ↦ Subtype.ext <| Module.ext <| funext₂ <| smul_one_smul S

Equivalence between ring homomorphisms and compatible module structures

Informal description

Given semirings $R$ and $S$, there is a natural equivalence between: 1. The type of ring homomorphisms from $R$ to $S$ ($R \to+* S$), and 2. The type of $R$-module structures on $S$ where $S$ forms a scalar tower over itself with $R$ (i.e., $\{ \text{Module } R S \text{ with } \text{IsScalarTower } R S S \}$). The equivalence is given by: - For a ring homomorphism $f: R \to+* S$, the corresponding module structure has scalar multiplication $r \bullet s = f(r) \cdot s$ - For a compatible module structure, the corresponding ring homomorphism is $r \mapsto r \bullet 1_S$