Documentation

TauCeti.Algebra.Homology.DG.Module.Right.Restriction.Basic

Restriction of scalars for differential graded right modules #

A morphism f : A โŸถ B of differential graded algebras turns every right DG B-module into a right DG A-module by the action x ยท a = x ยท f(a). This file packages that construction without installing a global module instance depending on f: the carrier is the wrapper TauCeti.DGRightModule.RestrictScalars f M.

Restriction preserves the underlying grading and differential. A morphism of right DG B-modules is therefore also a morphism after restriction, and this operation preserves identity maps and composition. These constructions are the underived restriction-of-scalars input for the DG categories of modules and their later derived functors.

Main definitions #

References #

source
structure TauCeti.DGRightModule.RestrictScalars {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (_f : DGAlgHom hA hB) (M : Type uM) :
Type uM

The carrier of a right module after restriction of scalars along a DG algebra morphism.

The wrapper keeps the restricted Aแตแต’แต–-module instance local to the chosen morphism f. Its additive group and R-module structures are those of M.

  • val : M

    The element of the original module underlying a restricted element.

Instances For
    source
    theorem TauCeti.DGRightModule.RestrictScalars.ext {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {f : DGAlgHom hA hB} {M : Type uM} {x y : RestrictScalars f M} (h : x.val = y.val) :
    x = y

    Restricted elements are equal when their underlying elements are equal.

    source
    theorem TauCeti.DGRightModule.RestrictScalars.ext_iff {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {f : DGAlgHom hA hB} {M : Type uM} {x y : RestrictScalars f M} :
    x = y โ†” x.val = y.val
    source
    @[instance_reducible]
    instance TauCeti.DGRightModule.RestrictScalars.instAddCommGroup {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] :
    AddCommGroup (RestrictScalars f M)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[instance_reducible]
    instance TauCeti.DGRightModule.RestrictScalars.instModule {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module R M] :
    Module R (RestrictScalars f M)
    Equations
    • One or more equations did not get rendered due to their size.
    source
    @[instance_reducible]
    instance TauCeti.DGRightModule.RestrictScalars.instModuleMulOpposite {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module Bแตแต’แต– M] :
    Module Aแตแต’แต– (RestrictScalars f M)

    The restricted right action: a : A acts through f a : B.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    def TauCeti.DGRightModule.RestrictScalars.linearEquiv {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module R M] :
    RestrictScalars f M โ‰ƒโ‚—[R] M

    The identity R-linear equivalence from a restricted module to its original carrier.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.DGRightModule.RestrictScalars.val_zero {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] :
      val 0 = 0
      source
      @[simp]
      theorem TauCeti.DGRightModule.RestrictScalars.val_add {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] (x y : RestrictScalars f M) :
      (x + y).val = x.val + y.val
      source
      @[simp]
      theorem TauCeti.DGRightModule.RestrictScalars.val_zsmul {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] (n : โ„ค) (x : RestrictScalars f M) :
      (n โ€ข x).val = n โ€ข x.val
      source
      @[simp]
      theorem TauCeti.DGRightModule.RestrictScalars.val_smul {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module R M] (r : R) (x : RestrictScalars f M) :
      (r โ€ข x).val = r โ€ข x.val
      source
      @[simp]
      theorem TauCeti.DGRightModule.RestrictScalars.linearEquiv_apply {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module R M] (x : RestrictScalars f M) :
      (linearEquiv f M) x = x.val
      source
      @[simp]
      theorem TauCeti.DGRightModule.RestrictScalars.linearEquiv_symm_apply {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module R M] (x : M) :
      (linearEquiv f M).symm x = { val := x }
      source
      theorem TauCeti.DGRightModule.RestrictScalars.val_op_smul {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module Bแตแต’แต– M] (a : A) (x : RestrictScalars f M) :
      (MulOpposite.op a โ€ข x).val = MulOpposite.op (f a) โ€ข x.val

      On underlying elements, restricted scalar multiplication is multiplication by the image under f.

      source
      @[simp]
      theorem TauCeti.DGRightModule.RestrictScalars.val_smul_eq {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module Bแตแต’แต– M] (a : Aแตแต’แต–) (x : RestrictScalars f M) :
      (a โ€ข x).val = (AlgHom.op โ†‘f.toGradedAlgHom) a โ€ข x.val

      On underlying elements, an opposite scalar acts through its image under f.

      source
      instance TauCeti.DGRightModule.RestrictScalars.instIsScalarTowerMulOpposite {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} (f : DGAlgHom hA hB) (M : Type uM) [AddCommGroup M] [Module R M] [Module Bแตแต’แต– M] [IsScalarTower R Bแตแต’แต– M] :
      IsScalarTower R Aแตแต’แต– (RestrictScalars f M)
      source
      noncomputable def TauCeti.IsDGRightModule.restrictScalarsGrading {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} [AddCommGroup M] [Module R M] {โ„ณ : โ„ค โ†’ Submodule R M} [DirectSum.Decomposition โ„ณ] (f : DGAlgHom hA hB) (q : โ„ค) :
      Submodule R (DGRightModule.RestrictScalars f M)

      The grading of a module does not change under restriction of scalars.

      Equations
      Instances For
        source
        @[simp]
        theorem TauCeti.IsDGRightModule.mem_restrictScalarsGrading_iff {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} [AddCommGroup M] [Module R M] {โ„ณ : โ„ค โ†’ Submodule R M} [DirectSum.Decomposition โ„ณ] (f : DGAlgHom hA hB) {q : โ„ค} {x : DGRightModule.RestrictScalars f M} :
        x โˆˆ restrictScalarsGrading f q โ†” (DGRightModule.RestrictScalars.linearEquiv f M) x โˆˆ โ„ณ q
        source
        @[instance_reducible]
        noncomputable instance TauCeti.IsDGRightModule.instDecompositionIntRestrictScalarsSubmoduleRestrictScalarsGrading {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} [AddCommGroup M] [Module R M] {โ„ณ : โ„ค โ†’ Submodule R M} [DirectSum.Decomposition โ„ณ] (f : DGAlgHom hA hB) :
        DirectSum.Decomposition (restrictScalarsGrading f)

        The transported grading of a restricted module remains a direct-sum decomposition.

        Equations
        • One or more equations did not get rendered due to their size.
        source
        instance TauCeti.IsDGRightModule.instGradedSMulIntSubmoduleMulOppositeRestrictScalarsPieceOppositeOfDecompositionRestrictScalarsGrading {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} [AddCommGroup M] [Module R M] [Module Bแตแต’แต– M] {โ„ณ : โ„ค โ†’ Submodule R M} [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece โ„ณ] [DirectSum.Decomposition โ„ณ] (f : DGAlgHom hA hB) :
        SetLike.GradedSMul (InternalGrading.ofDecomposition ๐’œ).opposite.piece (restrictScalarsGrading f)

        The restricted scalar action respects degrees because the algebra morphism is graded.

        source
        def TauCeti.IsDGRightModule.restrictScalarsDifferential {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} [AddCommGroup M] [Module R M] {dM : M โ†’โ‚—[R] M} (f : DGAlgHom hA hB) :
        DGRightModule.RestrictScalars f M โ†’โ‚—[R] DGRightModule.RestrictScalars f M

        The differential of a restricted module is its original differential.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.IsDGRightModule.val_restrictScalarsDifferential {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} [AddCommGroup M] [Module R M] {dM : M โ†’โ‚—[R] M} (f : DGAlgHom hA hB) (x : DGRightModule.RestrictScalars f M) :
          ((restrictScalarsDifferential f) x).val = dM x.val
          source
          theorem TauCeti.IsDGRightModule.restrictScalars {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} [AddCommGroup M] [Module R M] [Module Bแตแต’แต– M] [IsScalarTower R Bแตแต’แต– M] {โ„ณ : โ„ค โ†’ Submodule R M} [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} (f : DGAlgHom hA hB) (hM : IsDGRightModule hB โ„ณ dM) :
          IsDGRightModule hA (restrictScalarsGrading f) (restrictScalarsDifferential f)

          Restrict a right DG module along a morphism of DG algebras.

          source
          noncomputable def TauCeti.DGRightModuleHom.restrictScalars {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [Module Bแตแต’แต– M] [IsScalarTower R Bแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Bแตแต’แต– N] [IsScalarTower R Bแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece ๐’ฉ] [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule hB โ„ณ dM} {hN : IsDGRightModule hB ๐’ฉ dN} (f : DGAlgHom hA hB) (g : DGRightModuleHom hM hN) :
          DGRightModuleHom โ‹ฏ โ‹ฏ

          Restrict a morphism of right DG modules along a morphism of DG algebras.

          Equations
          Instances For
            source
            @[simp]
            theorem TauCeti.DGRightModuleHom.val_restrictScalars {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} {N : Type uN} [AddCommGroup M] [Module R M] [Module Bแตแต’แต– M] [IsScalarTower R Bแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Bแตแต’แต– N] [IsScalarTower R Bแตแต’แต– N] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece ๐’ฉ] [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {hM : IsDGRightModule hB โ„ณ dM} {hN : IsDGRightModule hB ๐’ฉ dN} (f : DGAlgHom hA hB) (g : DGRightModuleHom hM hN) (x : DGRightModule.RestrictScalars f M) :
            ((restrictScalars f g) x).val = g x.val
            source
            @[simp]
            theorem TauCeti.DGRightModuleHom.restrictScalars_id {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} [AddCommGroup M] [Module R M] [Module Bแตแต’แต– M] [IsScalarTower R Bแตแต’แต– M] {โ„ณ : โ„ค โ†’ Submodule R M} [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece โ„ณ] [DirectSum.Decomposition โ„ณ] {dM : M โ†’โ‚—[R] M} {hM : IsDGRightModule hB โ„ณ dM} (f : DGAlgHom hA hB) :
            restrictScalars f (DGRightModuleHom.id hM) = DGRightModuleHom.id โ‹ฏ

            Restriction of scalars preserves identity morphisms.

            source
            @[simp]
            theorem TauCeti.DGRightModuleHom.restrictScalars_comp {R : Type uR} {A : Type uA} {B : Type uB} [CommRing R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {M : Type uM} {N : Type uN} {P : Type uP} [AddCommGroup M] [Module R M] [Module Bแตแต’แต– M] [IsScalarTower R Bแตแต’แต– M] [AddCommGroup N] [Module R N] [Module Bแตแต’แต– N] [IsScalarTower R Bแตแต’แต– N] [AddCommGroup P] [Module R P] [Module Bแตแต’แต– P] [IsScalarTower R Bแตแต’แต– P] {โ„ณ : โ„ค โ†’ Submodule R M} {๐’ฉ : โ„ค โ†’ Submodule R N} {โ„ณP : โ„ค โ†’ Submodule R P} [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece โ„ณ] [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece ๐’ฉ] [SetLike.GradedSMul (InternalGrading.ofDecomposition โ„ฌ).opposite.piece โ„ณP] [DirectSum.Decomposition โ„ณ] [DirectSum.Decomposition ๐’ฉ] [DirectSum.Decomposition โ„ณP] {dM : M โ†’โ‚—[R] M} {dN : N โ†’โ‚—[R] N} {dP : P โ†’โ‚—[R] P} {hM : IsDGRightModule hB โ„ณ dM} {hN : IsDGRightModule hB ๐’ฉ dN} {hP : IsDGRightModule hB โ„ณP dP} (f : DGAlgHom hA hB) (g : DGRightModuleHom hN hP) (k : DGRightModuleHom hM hN) :
            restrictScalars f (g.comp k) = (restrictScalars f g).comp (restrictScalars f k)

            Restriction of scalars preserves composition.