Cokernels of closed maps of curved right modules

The cokernel of a closed map is the quotient by its image, with the quotient grading and the induced differential. The image is stable under the differential because the map is closed. The Leibniz and curvature laws descend to the quotient, and its projection is a cokernel in the existing closed category.

cokernelEquiv identifies the carrier of cokernelObj with the range quotient and provides its inherited right action. Its homogeneous elements are classes of homogeneous target elements, and its differential sends the class of an element to the class of its differential. cokernelIsColimit gives the universal property of the projection cokernelπ, and forgetDifferentialCokernelIso gives the graded comparison. These cokernels 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.cokernelDifferential {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) : N.carrier ⧸ (closedHom f).range →ₗ[R] N.carrier ⧸ (closedHom f).range

The target differential induces a differential on the quotient by the image.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.cokernelDifferential_mk {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 : N.carrier) : (cokernelDifferential f) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (N.differential x)

The induced differential sends the class of x to the class of its differential.

noncomputable def TauCeti.CurvedDGRightModuleCat.cokernelObj {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 quotient of the target by the image of a closed map.

noncomputable def TauCeti.CurvedDGRightModuleCat.cokernelEquiv {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) : (cokernelObj f).carrier ≃ₗ[Aᵐᵒᵖ] N.carrier ⧸ (closedHom f).range

The cokernel carrier is the range quotient. The equivalence's linearity supplies the inherited right action without exposing the construction of cokernelObj.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.cokernelEquiv_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 : (cokernelObj f).carrier) : (cokernelEquiv f) ((cokernelObj f).differential x) = (cokernelDifferential f) ((cokernelEquiv f) x)

The cokernel differential corresponds to the induced quotient differential.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.mem_cokernelObj_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 : (cokernelObj f).carrier} : x ∈ (cokernelObj f).grading p ↔ ∃ y ∈ N.grading p, Submodule.Quotient.mk y = (cokernelEquiv f) x

Homogeneous cokernel elements correspond to classes of homogeneous target elements.

noncomputable def TauCeti.CurvedDGRightModuleCat.cokernelπ {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) ℤ) N ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cokernelObj f)

The projection onto the curved cokernel is a closed map.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.hom_cokernelπ {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 (cokernelπ f) = ↑(cokernelEquiv f).symm ∘ₗ (closedHom f).range.mkQ

The underlying cokernel projection is the quotient map followed by its carrier comparison.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.comp_cokernelπ {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 f (cokernelπ f) = 0

The original map followed by its cokernel projection is zero.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.comp_cokernelπ_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) ℤ) (cokernelObj f) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (cokernelπ f) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

The original map followed by its cokernel projection is zero.

noncomputable def TauCeti.CurvedDGRightModuleCat.cokernelCocone {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.CokernelCofork f

The cokernel cofork in the closed category of curved right modules.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.cokernelCocone_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) : (cokernelCocone f).pt = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cokernelObj f)

The point of the sealed cokernel cofork is the characteristic cokernel object.

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.cokernelCocone_π {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.Limits.Cofork.π (cokernelCocone f)) (CategoryTheory.eqToHom ⋯) = cokernelπ f

The cokernel projection agrees with the characteristic projection after identifying its point.

noncomputable def TauCeti.CurvedDGRightModuleCat.cokernelIsColimit {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.IsColimit (cokernelCocone f)

The curved cokernel projection satisfies the cokernel universal property.

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

The closed category of curved right modules has cokernels.

noncomputable def TauCeti.CurvedDGRightModuleCat.forgetDifferentialCokernelIso {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) ℤ) (cokernelObj f)) ≅ GradedModuleCat.cokernelObj (forgetDifferential.map f)

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

@[simp]

theorem TauCeti.CurvedDGRightModuleCat.forgetDifferentialCokernelIso_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) : (forgetDifferentialCokernelIso f).hom.hom = ↑(cokernelEquiv f)

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

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

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