Forgetting the differential of curved right modules

The underlying graded right module is an object of the existing graded module category over the opposite algebra. Forgetting the differential of a closed map gives a faithful additive linear functor which reflects isomorphisms. Cohomological shift by n corresponds to grading shift by -n, since both replace the degree-p piece by the degree-(p + n) piece.

This functor detects the graded splittings used in the Frobenius exact structure on curved right modules. A graded splitting need not commute with the differentials.

References

• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6.
• The Tau Ceti contributors, TauCeti.Algebra.Category.GradedModuleCat.Abelian: the reflection of isomorphisms proof adapts the corresponding forgetful-functor proof.

@[implicit_reducible]

noncomputable def TauCeti.CurvedDGRightModuleCat.toGradedModuleCat {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) : GradedModuleCat ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ)

The underlying graded right module, viewed as a graded module over the opposite algebra.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.toGradedModuleCat_piece {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) (p : ℤ) : M.toGradedModuleCat.grading.piece ℤ p = M.grading p

Forgetting the differential preserves the homogeneous pieces.

theorem TauCeti.CurvedDGRightModuleCat.isHomogeneous_toGradedModuleCat_iff {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} {p : ℤ} (f : M.carrier →ₗ[Aᵐᵒᵖ] N.carrier) : LinearMap.IsHomogeneous f (M.toGradedModuleCat.grading.piece ℤ) (N.toGradedModuleCat.grading.piece ℤ) p ↔ f ∈ dgRightModuleCochains p

A right-linear map is homogeneous of degree p for the underlying graded modules exactly when it is a cochain of degree p between the curved modules.

theorem TauCeti.CurvedDGRightModuleCat.mem_dgRightModuleCochains_iff_isHomogeneous_shiftObj {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} {p : ℤ} (a : M.carrier →ₗ[Aᵐᵒᵖ] N.carrier) : a ∈ dgRightModuleCochains p ↔ LinearMap.IsHomogeneous a (M.toGradedModuleCat.grading.piece ℤ) ((N.toGradedModuleCat.shiftObj (-p)).grading.piece ℤ) 0

A degree-p cochain is a degree-zero map into the grading shift by -p.

@[implicit_reducible]

noncomputable def TauCeti.CurvedDGRightModuleCat.forgetDifferential {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.Functor (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) (GradedModuleCat ((InternalGrading.ofDecomposition 𝒜).opposite.piece ℤ))

Forget the differential of a curved module and the closedness of a degree-zero map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.forgetDifferential_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} (M : CurvedDGRightModuleCat h) : forgetDifferential.obj (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M) = M.toGradedModuleCat

The graded forgetful functor takes a curved module to its underlying graded right module.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.forgetDifferential_map_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 N : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : (forgetDifferential.map f).hom = closedHom f

The graded forgetful functor acts by the underlying right-linear map.

instance TauCeti.CurvedDGRightModuleCat.instFaithfulForgetEnrichmentCochainComplexModuleCatIntGradedModuleCatMulOppositePieceOppositeOfDecompositionForgetDifferential {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} : forgetDifferential.Faithful

noncomputable def TauCeti.CurvedDGRightModuleCat.closedIsoOfGradedIso {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 N : CurvedDGRightModuleCat h} (g : M.toGradedModuleCat ≅ N.toGradedModuleCat) (hd : ∀ (x : M.toGradedModuleCat.carrier), N.differential (g.hom.hom x) = g.hom.hom (M.differential x)) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ≅ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N

A graded isomorphism commuting with the differentials lifts to the closed category.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedIsoOfGradedIso_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 N : CurvedDGRightModuleCat h} (g : M.toGradedModuleCat ≅ N.toGradedModuleCat) (hd : ∀ (x : M.toGradedModuleCat.carrier), N.differential (g.hom.hom x) = g.hom.hom (M.differential x)) : closedHom (closedIsoOfGradedIso g hd).hom = g.hom.hom

The lifted graded isomorphism retains its forward underlying linear map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedIsoOfGradedIso_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 N : CurvedDGRightModuleCat h} (g : M.toGradedModuleCat ≅ N.toGradedModuleCat) (hd : ∀ (x : M.toGradedModuleCat.carrier), N.differential (g.hom.hom x) = g.hom.hom (M.differential x)) : closedHom (closedIsoOfGradedIso g hd).inv = g.inv.hom

The lifted graded isomorphism retains its inverse underlying linear map.

instance TauCeti.CurvedDGRightModuleCat.instReflectsIsomorphismsForgetEnrichmentCochainComplexModuleCatIntGradedModuleCatMulOppositePieceOppositeOfDecompositionForgetDifferential {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} : forgetDifferential.ReflectsIsomorphisms

instance TauCeti.CurvedDGRightModuleCat.instAdditiveForgetEnrichmentCochainComplexModuleCatIntGradedModuleCatMulOppositePieceOppositeOfDecompositionForgetDifferential {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} : forgetDifferential.Additive

instance TauCeti.CurvedDGRightModuleCat.instLinearForgetEnrichmentCochainComplexModuleCatIntGradedModuleCatMulOppositePieceOppositeOfDecompositionForgetDifferential {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.Functor.Linear R forgetDifferential

noncomputable def TauCeti.CurvedDGRightModuleCat.closedShiftFunctorCompForgetDifferentialIso {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 : ℤ) : (closedShiftFunctor n).comp forgetDifferential ≅ forgetDifferential.comp (GradedModuleCat.shiftFunctor (-n))

After forgetting the differential, cohomological shift by n is grading shift by -n.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedShiftFunctorCompForgetDifferentialIso_hom_app_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} (n : ℤ) (M : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) : ((closedShiftFunctorCompForgetDifferentialIso n).hom.app M).hom = LinearMap.id

The shift comparison acts by the identity on underlying right modules.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.closedShiftFunctorCompForgetDifferentialIso_inv_app_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} (n : ℤ) (M : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)) : ((closedShiftFunctorCompForgetDifferentialIso n).inv.app M).hom = LinearMap.id

The inverse shift comparison acts by the identity on underlying right modules.