Documentation

Mathlib.RingTheory.QuotSMulTop

Reducing a module modulo an element of the ring #

Given a commutative ring R and an element r : R, the association M ↦ M ⧸ rM extends to a functor on the category of R-modules. This functor is isomorphic to the functor of tensoring by R ⧸ (r) on either side, but can be more convenient to work with since we can work with quotient types instead of fiddling with simple tensors.

Tags #

module, commutative algebra

@[reducible, inline]
abbrev QuotSMulTop {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] :
Type u_1

An abbreviation for M⧸rM that keeps us from having to write (⊤ : Submodule R M) over and over to satisfy the typechecker.

Equations
Instances For
    def QuotSMulTop.congr {R : Type u_2} [CommRing R] (r : R) {M' : Type u_3} {M'' : Type u_4} [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M''] (e : M' ≃ₗ[R] M'') :

    If M' is isomorphic to M'' as R-modules, then M'⧸rM' is isomorphic to M''⧸rM''.

    Equations
    Instances For
      noncomputable def QuotSMulTop.equivQuotTensor {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] :

      Reducing a module modulo r is the same as left tensoring with R/(r).

      Equations
      Instances For
        noncomputable def QuotSMulTop.equivTensorQuot {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] :

        Reducing a module modulo r is the same as right tensoring with R/(r).

        Equations
        Instances For
          def QuotSMulTop.map {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] :

          The action of the functor QuotSMulTop r on morphisms.

          Equations
          Instances For
            @[simp]
            theorem QuotSMulTop.map_apply_mk {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (x : M) :
            theorem QuotSMulTop.map_comp_mkQ {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') :
            (map r) f ∘ₗ (r ).mkQ = (r ).mkQ ∘ₗ f
            @[simp]
            theorem QuotSMulTop.map_id {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] :
            @[simp]
            theorem QuotSMulTop.map_comp {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} {M'' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M''] (g : M' →ₗ[R] M'') (f : M →ₗ[R] M') :
            (map r) (g ∘ₗ f) = (map r) g ∘ₗ (map r) f
            theorem QuotSMulTop.equivQuotTensor_naturality_mk {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (x : M) :
            theorem QuotSMulTop.equivQuotTensor_naturality {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') :
            theorem QuotSMulTop.equivTensorQuot_naturality_mk {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') (x : M) :
            theorem QuotSMulTop.equivTensorQuot_naturality {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] (f : M →ₗ[R] M') :
            theorem QuotSMulTop.map_surjective {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] {f : M →ₗ[R] M'} (hf : Function.Surjective f) :
            theorem QuotSMulTop.map_exact {R : Type u_2} [CommRing R] (r : R) {M : Type u_1} {M' : Type u_3} {M'' : Type u_4} [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] [AddCommGroup M''] [Module R M''] {f : M →ₗ[R] M'} {g : M' →ₗ[R] M''} (hfg : Function.Exact f g) (hg : Function.Surjective g) :
            Function.Exact ((map r) f) ((map r) g)
            noncomputable def QuotSMulTop.tensorQuotSMulTopEquivQuotSMulTop {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) (M' : Type u_3) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] :

            Tensoring on the left and applying QuotSMulTop · r commute.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def QuotSMulTop.quotSMulTopTensorEquivQuotSMulTop {R : Type u_2} [CommRing R] (r : R) (M : Type u_1) (M' : Type u_3) [AddCommGroup M] [Module R M] [AddCommGroup M'] [Module R M'] :

              Tensoring on the right and applying QuotSMulTop · r commute.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                noncomputable def QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop {R : Type u_3} [CommRing R] (r : R) (M : Type u_1) [AddCommGroup M] [Module R M] (S : Type u_2) [CommRing S] [Algebra R S] :

                Let R be a commutative ring, M be an R-module, S be an R-algebra, then S ⊗[R] (M/rM) is isomorphic to (S ⊗[R] M)⧸r(S ⊗[R] M) as S-modules.

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