Documentation

TauCeti.Algebra.Homology.Curved.Module.Right.Frobenius

The Frobenius structure on curved right modules #

For the graded-split exact structure, the relatively projective and injective objects are exactly the contractible modules. A contraction gives extensions and lifts by taking the closed boundary of its composite with a graded retraction or section. Cones of identities provide enough such objects.

No centrality of the curvature or linearity of the differential over the algebra is assumed. The splittings used here are graded right-linear maps, while their closed boundaries commute with the curved differentials.

References #

source
theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isInjective_of_isZero_homotopy {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} {P : CurvedDGRightModuleCat h} (hP : CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R P)) :
gradedSplitExact.isInjective (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P)

A contractible module is injective relative to the graded-split exact structure.

source
theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isProjective_of_isZero_homotopy {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} {P : CurvedDGRightModuleCat h} (hP : CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R P)) :
gradedSplitExact.isProjective (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P)

A contractible module is projective relative to the graded-split exact structure.

source
noncomputable def TauCeti.CurvedDGRightModuleCat.coneIdentityInjectivePresentation {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) :
gradedSplitExact.InjectivePresentation (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M)

The injective presentation M → Cone(id M) → M[1].

Instances For
    source
    @[simp]
    theorem TauCeti.CurvedDGRightModuleCat.coneIdentityInjectivePresentation_I {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) :
    M.coneIdentityInjectivePresentation.I = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (cone (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M)))

    The injective object in the presentation is the cone of the identity.

    source
    @[simp]
    theorem TauCeti.CurvedDGRightModuleCat.coneIdentityInjectivePresentation_K {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) :
    M.coneIdentityInjectivePresentation.K = CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) (M.shift 1)

    The cokernel object in the presentation is the shifted module.

    source
    @[simp]
    theorem TauCeti.CurvedDGRightModuleCat.coneIdentityInjectivePresentation_i {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.CategoryStruct.comp M.coneIdentityInjectivePresentation.i (CategoryTheory.eqToHom ⋯) = coneInclusion (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M))

    After identifying its target, the presentation map is the identity-cone inclusion.

    source
    @[simp]
    theorem TauCeti.CurvedDGRightModuleCat.coneIdentityInjectivePresentation_p {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.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp M.coneIdentityInjectivePresentation.p (CategoryTheory.eqToHom ⋯)) = coneProjection (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M))

    After identifying its endpoints, the presentation map is the identity-cone projection.

    source
    theorem TauCeti.CurvedDGRightModuleCat.exists_gradedSplitExact_isDeflation_contractible {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) :
    ∃ (P : CurvedDGRightModuleCat h) (p : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) P ⟶ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M), gradedSplitExact.IsDeflation p ∧ CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R P)

    Every curved module is a graded-split quotient of a contractible cone of an identity.

    source
    theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_enoughInjectives {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} :
    gradedSplitExact.EnoughInjectives

    The graded-split exact structure has enough relative injectives.

    source
    theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_enoughProjectives {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} :
    gradedSplitExact.EnoughProjectives

    The graded-split exact structure has enough relative projectives.

    source
    theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isInjective_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 : CurvedDGRightModuleCat h) :
    gradedSplitExact.isInjective (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M) ↔ CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R M)

    The relatively injective modules are exactly the contractible modules.

    source
    theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isProjective_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 : CurvedDGRightModuleCat h) :
    gradedSplitExact.isProjective (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) ℤ) M) ↔ CategoryTheory.Limits.IsZero (DGHomotopyCategory.of R M)

    The relatively projective modules are exactly the contractible modules.

    source
    theorem TauCeti.CurvedDGRightModuleCat.gradedSplitExact_isFrobenius {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} :
    gradedSplitExact.IsFrobenius

    The graded-split exact structure on curved right modules is Frobenius.