Kernels of closed maps of curved right modules

The kernel of a closed map has the inherited grading and the restricted differential. The closedness of the map makes its kernel stable under the differential; the Leibniz and curvature laws restrict to this submodule. Its inclusion is a kernel in the existing closed category.

kernelEquiv identifies the carrier of kernelObj with the kernel submodule and provides its inherited right action. The grading and differential equations characterize this curved object, and kernelIsLimit gives the universal property of its inclusion kernelι. forgetDifferentialKernelIso identifies its underlying graded object with the graded kernel. These kernels and their preservation are used by the graded-split exact structure.

References

• The Tau Ceti contributors, TauCeti.Algebra.Category.GradedModuleCat.Abelian.
• L. Positselski, Differential graded Koszul duality: an introductory survey, Section 7.6.

noncomputable def TauCeti.CurvedDGRightModuleCat.kernelDifferential {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) : ↥(closedHom f).ker →ₗ[R] ↥(closedHom f).ker

The differential restricted to the kernel of a closed map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.coe_kernelDifferential {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) (x : ↥(closedHom f).ker) : ↑((kernelDifferential f) x) = M.differential ↑x

The restricted differential is the source differential on underlying elements.

noncomputable def TauCeti.CurvedDGRightModuleCat.kernelObj {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) : CurvedDGRightModuleCat h

The curved module carried by the kernel of a closed map.

noncomputable def TauCeti.CurvedDGRightModuleCat.kernelEquiv {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) : (kernelObj f).carrier ≃ₗ[Aᵐᵒᵖ] ↥(closedHom f).ker

The kernel carrier is the kernel submodule. Its linearity characterizes the inherited right action; consumers use this equivalence rather than unfolding kernelObj.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.kernelEquiv_differential {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) (x : (kernelObj f).carrier) : (kernelEquiv f) ((kernelObj f).differential x) = (kernelDifferential f) ((kernelEquiv f) x)

The kernel's differential corresponds to the restricted source differential.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.mem_kernelObj_grading_iff {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) {p : ℤ} {x : (kernelObj f).carrier} : x ∈ (kernelObj f).grading p ↔ ↑((kernelEquiv f) x) ∈ M.grading p

Homogeneity in the curved kernel is homogeneity in the source under its carrier comparison.

noncomputable def TauCeti.CurvedDGRightModuleCat.kernelι {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) : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (kernelObj f) ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M

The inclusion of the curved kernel is a closed map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.hom_kernelι {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) : closedHom (kernelι f) = (closedHom f).ker.subtype ∘ₗ ↑(kernelEquiv f)

The underlying kernel inclusion is its carrier comparison followed by subtype inclusion.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.kernelι_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} {M N : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N) : CategoryTheory.CategoryStruct.comp (kernelι f) f = 0

The kernel inclusion followed by the original map is zero.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.kernelι_comp_assoc {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) {Z : CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h)} (h✝ : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) N ⟶ Z) : CategoryTheory.CategoryStruct.comp (kernelι f) (CategoryTheory.CategoryStruct.comp f h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The kernel inclusion followed by the original map is zero.

noncomputable def TauCeti.CurvedDGRightModuleCat.kernelCone {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) : CategoryTheory.Limits.KernelFork f

The kernel fork in the closed category of curved right modules.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.kernelCone_pt {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) : (kernelCone f).pt = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (kernelObj f)

The point of the sealed kernel fork is the characteristic kernel object.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.kernelCone_ι {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) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.Limits.Fork.ι (kernelCone f)) = kernelι f

The kernel fork's projection is the characteristic inclusion after identifying its point.

noncomputable def TauCeti.CurvedDGRightModuleCat.kernelIsLimit {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) : CategoryTheory.Limits.IsLimit (kernelCone f)

The curved kernel inclusion satisfies the kernel universal property.

instance TauCeti.CurvedDGRightModuleCat.instHasKernelsForgetEnrichmentCochainComplexModuleCatInt {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.Limits.HasKernels (CategoryTheory.ForgetEnrichment (CochainComplex (ModuleCat R) ℤ) (CurvedDGRightModuleCat h))

The closed category of curved right modules has kernels.

noncomputable def TauCeti.CurvedDGRightModuleCat.forgetDifferentialKernelIso {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.obj (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (kernelObj f)) ≅ GradedModuleCat.kernelObj (forgetDifferential.map f)

Forgetting the differential of the curved kernel gives the usual graded kernel.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.forgetDifferentialKernelIso_hom_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) : (forgetDifferentialKernelIso f).hom.hom = ↑(kernelEquiv f)

The graded comparison is the kernel's characteristic carrier equivalence.

instance TauCeti.CurvedDGRightModuleCat.instPreservesLimitForgetEnrichmentCochainComplexModuleCatIntGradedModuleCatMulOppositePieceOppositeOfDecompositionWalkingParallelPairParallelPairOfNatHomOfForgetDifferential {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) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) forgetDifferential

The graded forgetful functor preserves the kernel of a closed map.