Documentation

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

Restriction functors for differential graded right modules #

Restriction along a DG algebra morphism defines a faithful linear functor between the categories of right DG modules. Restriction along the identity is naturally isomorphic to the identity functor, and restriction along a composite is naturally isomorphic to successive restriction. These comparisons identify the carrier wrappers introduced by restriction, and preserve both the internal grading and the differential. They provide the ordinary categorical restriction side of extension/restriction of scalars.

The construction follows the change-of-rings interface of Mathlib's ModuleCat.restrictScalarsId and ModuleCat.restrictScalarsComp, with the additional grading and differential conditions of DG modules.

References #

source
noncomputable def TauCeti.DGRightModuleCat.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) :
CategoryTheory.Functor (DGRightModuleCat hB) (DGRightModuleCat hA)

Restriction of scalars along a DG algebra morphism, on the ordinary categories of DG modules. The action on each image object is given by the original action through the algebra morphism.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def TauCeti.DGRightModuleCat.restrictScalarsEquiv {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 : DGRightModuleCat hB) :
    ((restrictScalars f).obj M).carrier โ‰ƒโ‚—[R] M.carrier

    Restriction of scalars preserves the underlying module over the ground ring.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.restrictScalarsEquiv_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 : DGRightModuleCat hB) (a : Aแตแต’แต–) (x : ((restrictScalars f).obj M).carrier) :
      (restrictScalarsEquiv f M) (a โ€ข x) = MulOpposite.op (f (MulOpposite.unop a)) โ€ข (restrictScalarsEquiv f M) x

      The restricted action is the original action through the algebra morphism.

      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.restrictScalars_map_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 N : DGRightModuleCat hB} (g : M โŸถ N) (x : ((restrictScalars f).obj M).carrier) :
      (restrictScalarsEquiv f N) (((restrictScalars f).map g) x) = g ((restrictScalarsEquiv f M) x)

      Restricted morphisms act by the original morphism on underlying elements.

      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.mem_restrictScalars_obj_grading {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 : DGRightModuleCat hB) (q : โ„ค) (x : ((restrictScalars f).obj M).carrier) :
      x โˆˆ ((restrictScalars f).obj M).grading q โ†” (restrictScalarsEquiv f M) x โˆˆ M.grading q

      Restriction preserves the homogeneous pieces on underlying elements.

      source
      @[simp]
      theorem TauCeti.DGRightModuleCat.restrictScalarsEquiv_differential {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 : DGRightModuleCat hB) (x : ((restrictScalars f).obj M).carrier) :
      (restrictScalarsEquiv f M) (((restrictScalars f).obj M).differential x) = M.differential ((restrictScalarsEquiv f M) x)

      Restriction preserves the differential on underlying elements.

      source
      instance TauCeti.DGRightModuleCat.instFaithfulRestrictScalars {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) :
      (restrictScalars f).Faithful
      source
      instance TauCeti.DGRightModuleCat.instAdditiveRestrictScalars {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) :
      (restrictScalars f).Additive
      source
      instance TauCeti.DGRightModuleCat.instLinearRestrictScalars {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) :
      CategoryTheory.Functor.Linear R (restrictScalars f)
      source
      noncomputable def TauCeti.DGRightModuleCat.restrictScalarsIdApp {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {dA : A โ†’โ‚—[R] A} {hA : IsDGAlgebra ๐’œ dA} (M : DGRightModuleCat hA) :
      (restrictScalars (DGAlgHom.id hA)).obj M โ‰… M

      Restricting along the identity DG algebra morphism recovers the original module.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem TauCeti.DGRightModuleCat.restrictScalarsIdApp_hom_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {dA : A โ†’โ‚—[R] A} {hA : IsDGAlgebra ๐’œ dA} (M : DGRightModuleCat hA) (x : ((restrictScalars (DGAlgHom.id hA)).obj M).carrier) :
        M.restrictScalarsIdApp.hom x = (restrictScalarsEquiv (DGAlgHom.id hA) M) x
        source
        @[simp]
        theorem TauCeti.DGRightModuleCat.restrictScalarsIdApp_inv_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {dA : A โ†’โ‚—[R] A} {hA : IsDGAlgebra ๐’œ dA} (M : DGRightModuleCat hA) (x : M.carrier) :
        (restrictScalarsEquiv (DGAlgHom.id hA) M) (M.restrictScalarsIdApp.inv x) = x
        source
        noncomputable def TauCeti.DGRightModuleCat.restrictScalarsId {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {dA : A โ†’โ‚—[R] A} {hA : IsDGAlgebra ๐’œ dA} :
        restrictScalars (DGAlgHom.id hA) โ‰… CategoryTheory.Functor.id (DGRightModuleCat hA)

        Restriction along the identity is naturally isomorphic to the identity functor.

        Equations
        Instances For
          source
          @[simp]
          theorem TauCeti.DGRightModuleCat.restrictScalarsId_app {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {dA : A โ†’โ‚—[R] A} {hA : IsDGAlgebra ๐’œ dA} (M : DGRightModuleCat hA) :
          restrictScalarsId.app M = M.restrictScalarsIdApp
          source
          noncomputable def TauCeti.DGRightModuleCat.restrictScalarsCompApp {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] [GradedAlgebra ๐’ž] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} (f : DGAlgHom hA hB) (g : DGAlgHom hB hC) (M : DGRightModuleCat hC) :
          (restrictScalars (g.comp f)).obj M โ‰… (restrictScalars f).obj ((restrictScalars g).obj M)

          Restriction along a composite agrees with successive restriction on each module.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem TauCeti.DGRightModuleCat.restrictScalarsCompApp_hom_apply {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] [GradedAlgebra ๐’ž] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} (f : DGAlgHom hA hB) (g : DGAlgHom hB hC) (M : DGRightModuleCat hC) (x : ((restrictScalars (g.comp f)).obj M).carrier) :
            (restrictScalarsEquiv g M) ((restrictScalarsEquiv f ((restrictScalars g).obj M)) ((restrictScalarsCompApp f g M).hom x)) = (restrictScalarsEquiv (g.comp f) M) x
            source
            @[simp]
            theorem TauCeti.DGRightModuleCat.restrictScalarsCompApp_inv_apply {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] [GradedAlgebra ๐’ž] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} (f : DGAlgHom hA hB) (g : DGAlgHom hB hC) (M : DGRightModuleCat hC) (x : ((restrictScalars f).obj ((restrictScalars g).obj M)).carrier) :
            (restrictScalarsEquiv (g.comp f) M) ((restrictScalarsCompApp f g M).inv x) = (restrictScalarsEquiv g M) ((restrictScalarsEquiv f ((restrictScalars g).obj M)) x)
            source
            noncomputable def TauCeti.DGRightModuleCat.restrictScalarsComp {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] [GradedAlgebra ๐’ž] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} (f : DGAlgHom hA hB) (g : DGAlgHom hB hC) :
            restrictScalars (g.comp f) โ‰… (restrictScalars g).comp (restrictScalars f)

            Restriction along a composite is naturally isomorphic to successive restriction.

            Equations
            Instances For
              source
              @[simp]
              theorem TauCeti.DGRightModuleCat.restrictScalarsComp_app {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} [CommRing R] [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] {๐’œ : โ„ค โ†’ Submodule R A} {โ„ฌ : โ„ค โ†’ Submodule R B} {๐’ž : โ„ค โ†’ Submodule R C} [GradedAlgebra ๐’œ] [GradedAlgebra โ„ฌ] [GradedAlgebra ๐’ž] {dA : A โ†’โ‚—[R] A} {dB : B โ†’โ‚—[R] B} {dC : C โ†’โ‚—[R] C} {hA : IsDGAlgebra ๐’œ dA} {hB : IsDGAlgebra โ„ฌ dB} {hC : IsDGAlgebra ๐’ž dC} (f : DGAlgHom hA hB) (g : DGAlgHom hB hC) (M : DGRightModuleCat hC) :
              (restrictScalarsComp f g).app M = restrictScalarsCompApp f g M