Documentation

Mathlib.Algebra.Module.RingHom

Composing modules with a ring hom #

Main definitions #

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
    Instances For
      @[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
        Instances For
          @[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
            Instances For
              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
                Instances For
                  @[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) :
                  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
                    Instances For