Documentation

TauCeti.Algebra.Homology.Curved.Module.Right.Shift

Cohomological shifts of curved differential graded right modules #

The shift by n : โ„ค keeps the underlying right module, replaces the degree-p piece by the degree-(p + n) piece, and multiplies the differential by (-1)^n. The right action is unchanged. The sign in the differential compensates for the change of degree in the right Leibniz rule, and its square is still right multiplication by the same curvature, without a centrality hypothesis.

On homogeneous cochains of degree p, the DG shift multiplies the underlying map by (-1)^(n * p). In particular it keeps closed degree-zero maps and negates odd homotopies when n = 1.

References #

source
@[implicit_reducible]
noncomputable def TauCeti.CurvedDGRightModuleCat.shift {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (n : โ„ค) :
CurvedDGRightModuleCat h

The cohomological shift: M[n]แต– = Mแต–โบโฟ, with differential (-1)^n dM and unchanged right action and curvature.

Instances For
    source
    @[simp]
    theorem TauCeti.CurvedDGRightModuleCat.shift_grading {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (n p : โ„ค) :
    (M.shift n).grading p = M.grading (p + n)

    Shifting replaces the degree-p piece by the degree-(p + n) piece.

    source
    @[simp]
    theorem TauCeti.CurvedDGRightModuleCat.shift_differential_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (n : โ„ค) (x : M.carrier) :
    (M.shift n).differential x = n.negOnePow โ€ข M.differential x

    The differential of the shift acts by the shift sign.

    source
    noncomputable def TauCeti.CurvedDGRightModuleCat.shiftCochain {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (N : CurvedDGRightModuleCat h) (n p : โ„ค) :
    โ†ฅ(dgRightModuleCochains p) โ†’โ‚—[R] โ†ฅ(dgRightModuleCochains p)

    The shift on degree-p cochains, with the sign (-1)^(n * p) that makes it commute with the Hom differential.

    Instances For
      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.shiftCochain_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (N : CurvedDGRightModuleCat h) (n p : โ„ค) (f : โ†ฅ(dgRightModuleCochains p)) (x : M.carrier) :
      โ†‘((M.shiftCochain N n p) f) x = (n * p).negOnePow โ€ข โ†‘f x

      On underlying maps the cochain shift is multiplication by its Koszul sign.

      source
      theorem TauCeti.CurvedDGRightModuleCat.shiftCochain_curvedDifferential {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (N : CurvedDGRightModuleCat h) (n p : โ„ค) (f : โ†ฅ(dgRightModuleCochains p)) :
      (M.shiftCochain N n (p + 1)) ((dgRightModuleCochains.curvedDifferential p) f) = (dgRightModuleCochains.curvedDifferential p) ((M.shiftCochain N n p) f)

      Shifting cochains commutes with the Hom differential.

      source
      theorem TauCeti.CurvedDGRightModuleCat.shift_one_differential_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (x : M.carrier) :
      (M.shift 1).differential x = -M.differential x

      The shift by one negates the differential.

      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.shiftCochain_zero {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (N : CurvedDGRightModuleCat h) (n : โ„ค) (f : โ†ฅ(dgRightModuleCochains 0)) :
      โ†‘((M.shiftCochain N n 0) f) = โ†‘f

      The shift leaves degree-zero underlying maps unchanged.

      source
      theorem TauCeti.CurvedDGRightModuleCat.shiftCochain_neg_one_apply {R : Type uR} {A : Type uA} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (N : CurvedDGRightModuleCat h) (n : โ„ค) (k : โ†ฅ(dgRightModuleCochains (-1))) (x : M.carrier) :
      โ†‘((M.shiftCochain N n (-1)) k) x = n.negOnePow โ€ข โ†‘k x

      The shift multiplies an odd homotopy by (-1)^n.

      The DG shift functor and its induced functors #

      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.shiftCochain_id {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) (M : CurvedDGRightModuleCat h) :
      (M.shiftCochain M n 0) dgRightModuleCochains.id = dgRightModuleCochains.id

      The shift preserves identity cochains.

      source
      theorem TauCeti.CurvedDGRightModuleCat.shiftCochain_comp {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) {M N P : CurvedDGRightModuleCat h} {p q r : โ„ค} (g : โ†ฅ(dgRightModuleCochains p)) (f : โ†ฅ(dgRightModuleCochains q)) (hpq : p + q = r) :
      (M.shiftCochain P n r) (dgRightModuleCochains.comp g f hpq) = dgRightModuleCochains.comp ((N.shiftCochain P n p) g) ((M.shiftCochain N n q) f) hpq

      The shift preserves composition of homogeneous cochains.

      source
      noncomputable def TauCeti.CurvedDGRightModuleCat.shiftDGMap {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n p : โ„ค) {M N : CurvedDGRightModuleCat h} :
      DGHom R p M N โ†’โ‚—[R] DGHom R p (M.shift n) (N.shift n)

      The action of the shift on homogeneous morphisms of the existing DG category.

      Instances For
        source
        @[simp]
        theorem TauCeti.CurvedDGRightModuleCat.dgHomLinearEquivCochains_shiftDGMap {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n p : โ„ค) {M N : CurvedDGRightModuleCat h} (f : DGHom R p M N) :
        ((M.shift n).dgHomLinearEquivCochains (N.shift n) p) ((shiftDGMap n p) f) = (M.shiftCochain N n p) ((M.dgHomLinearEquivCochains N p) f)

        Transport to cochains identifies the DG shift action with the signed cochain shift.

        source
        theorem TauCeti.CurvedDGRightModuleCat.shiftDGMap_dgDifferential {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n p : โ„ค) {M N : CurvedDGRightModuleCat h} (f : DGHom R p M N) :
        (shiftDGMap n (p + 1)) ((dgDifferential R p) f) = (dgDifferential R p) ((shiftDGMap n p) f)

        The DG shift action commutes with the differential.

        source
        theorem TauCeti.CurvedDGRightModuleCat.shiftDGMap_dgId {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) (M : CurvedDGRightModuleCat h) :
        (shiftDGMap n 0) (dgId R M) = dgId R (M.shift n)

        The DG shift action preserves identities.

        source
        theorem TauCeti.CurvedDGRightModuleCat.shiftDGMap_dgComp {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) {M N P : CurvedDGRightModuleCat h} {p q r : โ„ค} (f : DGHom R p M N) (g : DGHom R q N P) (hpq : p + q = r) :
        (shiftDGMap n r) (dgComp R f g hpq) = dgComp R ((shiftDGMap n p) f) ((shiftDGMap n q) g) hpq

        The DG shift action preserves composition in Mathlib's enriched factor order.

        source
        @[implicit_reducible]
        noncomputable def TauCeti.CurvedDGRightModuleCat.dgShiftFunctor {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) :
        CategoryTheory.EnrichedFunctor (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h) (CurvedDGRightModuleCat h)

        The cohomological shift as a DG endofunctor of curved right modules.

        Instances For
          source
          @[simp]
          theorem TauCeti.CurvedDGRightModuleCat.dgShiftFunctor_obj {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) (M : CurvedDGRightModuleCat h) :
          (dgShiftFunctor n).obj M = M.shift n

          The DG shift sends a module to its explicit cohomological shift.

          source
          @[simp]
          theorem TauCeti.CurvedDGRightModuleCat.dgShiftFunctor_dgMap {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n p : โ„ค) {M N : CurvedDGRightModuleCat h} (f : DGHom R p M N) :
          ((dgShiftFunctor n).dgMap p) f = (shiftDGMap n p) f

          The DG shift acts on homogeneous morphisms by the signed cochain shift.

          source
          @[implicit_reducible]
          noncomputable def TauCeti.CurvedDGRightModuleCat.closedShiftFunctor {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) :
          CategoryTheory.Functor (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h)) (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h))

          The cohomological shift on the closed degree-zero category of curved modules.

          Instances For
            source
            @[simp]
            theorem TauCeti.CurvedDGRightModuleCat.closedShiftFunctor_obj_of {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) (M : CurvedDGRightModuleCat h) :
            (closedShiftFunctor n).obj (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M) = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) (M.shift n)

            The closed shift sends a module to its explicit shift.

            source
            @[simp]
            theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedShiftFunctor_map {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) {M N : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N) :
            closedHom ((closedShiftFunctor n).map f) = closedHom f

            On closed morphisms the shift keeps the underlying right-linear map.

            Zero and addition comparisons in the closed category #

            source
            noncomputable def TauCeti.CurvedDGRightModuleCat.closedShiftZeroIso {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) :
            CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) (M.shift 0) โ‰… CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M

            A module shifted by zero is canonically isomorphic to the original module.

            Instances For
              source
              noncomputable def TauCeti.CurvedDGRightModuleCat.closedShiftAddIso {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (n m : โ„ค) :
              CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) (M.shift (n + m)) โ‰… CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) ((M.shift n).shift m)

              Successive cohomological shifts add their amounts.

              Instances For
                source
                @[simp]
                theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedShiftZeroIso_hom {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) :
                closedHom M.closedShiftZeroIso.hom = LinearMap.id

                The zero-shift comparison has identity underlying map.

                source
                @[simp]
                theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedShiftZeroIso_inv {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) :
                closedHom M.closedShiftZeroIso.inv = LinearMap.id

                The inverse zero-shift comparison has identity underlying map.

                source
                @[simp]
                theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedShiftAddIso_hom {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (n m : โ„ค) :
                closedHom (M.closedShiftAddIso n m).hom = LinearMap.id

                The addition comparison has identity underlying map.

                source
                @[simp]
                theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedShiftAddIso_inv {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (n m : โ„ค) :
                closedHom (M.closedShiftAddIso n m).inv = LinearMap.id

                The inverse addition comparison has identity underlying map.

                source
                noncomputable def TauCeti.CurvedDGRightModuleCat.closedShiftFunctorZeroIso {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} :
                closedShiftFunctor 0 โ‰… CategoryTheory.Functor.id (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h))

                Shifting closed modules by zero is naturally isomorphic to the identity.

                Instances For
                  source
                  noncomputable def TauCeti.CurvedDGRightModuleCat.closedShiftFunctorAddIso {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n m : โ„ค) :
                  closedShiftFunctor (n + m) โ‰… (closedShiftFunctor n).comp (closedShiftFunctor m)

                  The addition comparisons are natural in closed morphisms.

                  Instances For
                    source
                    @[simp]
                    theorem TauCeti.CurvedDGRightModuleCat.closedShiftFunctorZeroIso_hom_app {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h)) :
                    closedShiftFunctorZeroIso.hom.app X = (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) โ„ค) X).closedShiftZeroIso.hom

                    The zero comparison is the canonical object comparison.

                    source
                    @[simp]
                    theorem TauCeti.CurvedDGRightModuleCat.closedShiftFunctorZeroIso_inv_app {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h)) :
                    closedShiftFunctorZeroIso.inv.app X = (CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) โ„ค) X).closedShiftZeroIso.inv

                    The inverse zero comparison is the canonical object comparison.

                    source
                    @[simp]
                    theorem TauCeti.CurvedDGRightModuleCat.closedShiftFunctorAddIso_hom_app {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n m : โ„ค) (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h)) :
                    (closedShiftFunctorAddIso n m).hom.app X = ((CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) โ„ค) X).closedShiftAddIso n m).hom

                    The addition comparison is the canonical object comparison.

                    source
                    @[simp]
                    theorem TauCeti.CurvedDGRightModuleCat.closedShiftFunctorAddIso_inv_app {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n m : โ„ค) (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h)) :
                    (closedShiftFunctorAddIso n m).inv.app X = ((CategoryTheory.ForgetEnrichment.to (CochainComplex (ModuleCat R) โ„ค) X).closedShiftAddIso n m).inv

                    The inverse addition comparison is the canonical object comparison.

                    source
                    @[simp]
                    theorem TauCeti.CurvedDGRightModuleCat.closedHom_eqToHom_shift {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (n m : โ„ค) (hnm : n = m) :
                    closedHom (CategoryTheory.eqToHom โ‹ฏ) = LinearMap.id

                    Transport along equality of shift amounts has identity underlying map.

                    source
                    @[instance_reducible]
                    noncomputable instance TauCeti.CurvedDGRightModuleCat.instHasShiftForgetEnrichmentCochainComplexModuleCatInt {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} :
                    CategoryTheory.HasShift (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h)) โ„ค

                    The cohomological shifts form a coherent integer shift on the closed category.

                    source
                    @[implicit_reducible]
                    noncomputable def TauCeti.CurvedDGRightModuleCat.homotopyShiftFunctor {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) :
                    CategoryTheory.Functor (DGHomotopyCategory R (CurvedDGRightModuleCat h)) (DGHomotopyCategory R (CurvedDGRightModuleCat h))

                    The cohomological shift on the existing curved homotopy category.

                    Instances For
                      source
                      instance TauCeti.CurvedDGRightModuleCat.instAdditiveDGHomotopyCategoryHomotopyShiftFunctor {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) :
                      (homotopyShiftFunctor n).Additive
                      source
                      instance TauCeti.CurvedDGRightModuleCat.instLinearDGHomotopyCategoryHomotopyShiftFunctor {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) :
                      CategoryTheory.Functor.Linear R (homotopyShiftFunctor n)
                      source
                      @[simp]
                      theorem TauCeti.CurvedDGRightModuleCat.homotopyShiftFunctor_obj_of {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) (M : CurvedDGRightModuleCat h) :
                      (homotopyShiftFunctor n).obj (DGHomotopyCategory.of R M) = DGHomotopyCategory.of R (M.shift n)

                      The homotopy shift sends the class of a module to the class of its explicit shift.

                      source
                      theorem TauCeti.CurvedDGRightModuleCat.shiftDGMap_mem_dgCycles {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) {M N : CurvedDGRightModuleCat h} {f : DGHom R 0 M N} (hf : f โˆˆ dgCycles R M N) :
                      (shiftDGMap n 0) f โˆˆ dgCycles R (M.shift n) (N.shift n)

                      The signed shift of a closed DG morphism is closed.

                      source
                      @[simp]
                      theorem TauCeti.CurvedDGRightModuleCat.homotopyShiftFunctor_map_homOf {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) {M N : CurvedDGRightModuleCat h} (f : DGHom R 0 M N) (hf : f โˆˆ dgCycles R M N) :
                      (homotopyShiftFunctor n).map (DGHomotopyCategory.homOf R f hf) = DGHomotopyCategory.homOf R ((shiftDGMap n 0) f) โ‹ฏ

                      The homotopy shift maps a represented closed morphism to its shifted representative.

                      The coherent shift on the curved homotopy category #

                      source
                      @[instance_reducible]
                      noncomputable instance TauCeti.CurvedDGRightModuleCat.instHasShiftDGHomotopyCategoryInt {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} :
                      CategoryTheory.HasShift (DGHomotopyCategory R (CurvedDGRightModuleCat h)) โ„ค

                      The integer shifts descend to the existing homotopy category, with coherence supplied by Mathlib's induced-shift construction.

                      source
                      @[instance_reducible]
                      noncomputable instance TauCeti.CurvedDGRightModuleCat.instCommShiftForgetEnrichmentCochainComplexModuleCatIntDGHomotopyCategoryDgClosedToHomotopy {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} :
                      (dgClosedToHomotopy R).CommShift โ„ค

                      The quotient functor commutes with the coherent integer shifts.

                      source
                      @[simp]
                      theorem TauCeti.CurvedDGRightModuleCat.dgClosedToHomotopy_commShiftIso_hom_app {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) (X : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) โ„ค) (CurvedDGRightModuleCat h)) :
                      (CategoryTheory.Functor.commShiftIso (dgClosedToHomotopy R) n).hom.app X = CategoryTheory.eqToHom โ‹ฏ

                      The quotient-shift comparison is the identity transport on the underlying shifted module, for every integer shift.

                      source
                      theorem TauCeti.CurvedDGRightModuleCat.homotopyShiftFunctor_map_quotient {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) {M N : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N) :
                      (homotopyShiftFunctor n).map ((dgClosedToHomotopy R).map f) = (dgClosedToHomotopy R).map ((closedShiftFunctor n).map f)

                      Shifting the class of a closed map is the class of its closed shift.

                      source
                      @[simp]
                      theorem TauCeti.CurvedDGRightModuleCat.shiftFunctor_eq_homotopyShiftFunctor {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) :
                      CategoryTheory.shiftFunctor (DGHomotopyCategory R (CurvedDGRightModuleCat h)) n = homotopyShiftFunctor n

                      The categorical integer shift is the explicitly constructed homotopy shift.

                      source
                      instance TauCeti.CurvedDGRightModuleCat.instAdditiveDGHomotopyCategoryShiftFunctorInt {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) :
                      (CategoryTheory.shiftFunctor (DGHomotopyCategory R (CurvedDGRightModuleCat h)) n).Additive
                      source
                      instance TauCeti.CurvedDGRightModuleCat.instLinearDGHomotopyCategoryShiftFunctorInt {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (n : โ„ค) :
                      CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor (DGHomotopyCategory R (CurvedDGRightModuleCat h)) n)
                      source
                      theorem TauCeti.CurvedDGRightModuleCat.shift_of {R A : Type u} [CommRing R] [Ring A] [Algebra R A] {๐’œ : โ„ค โ†’ Submodule R A} [GradedAlgebra ๐’œ] {d : A โ†’โ‚—[R] A} {w : A} {h : IsCurvedDGAlgebra ๐’œ d w} (M : CurvedDGRightModuleCat h) (n : โ„ค) :
                      DGHomotopyCategory.of R MโŸฆnโŸง = DGHomotopyCategory.of R (M.shift n)

                      A categorical shift of a module class is its explicit cohomological shift.