Documentation

TauCeti.Algebra.Homology.Curved.Module.Right.ClosedCategory

Closed morphisms of curved differential graded right modules #

This file gives element-level constructors and computations for Mathlib's closed degree-zero category of the existing curved DG enrichment. A closed morphism is a right-linear map that preserves the internal grading and commutes with the module differentials. A right-linear equivalence preserving the grading and differential gives an isomorphism in that category.

The category and its morphisms remain CategoryTheory.ForgetEnrichment; the constructors use the existing identification with zero-cocycles of the curved Hom complex.

source
noncomputable def TauCeti.CurvedDGRightModuleCat.closedHom {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) :
M.carrier โ†’โ‚—[Aแตแต’แต–] N.carrier

The underlying right-linear map of a morphism in the closed degree-zero category.

Instances For
    source
    theorem TauCeti.CurvedDGRightModuleCat.closedHom_eq {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 = โ†‘((M.dgHomLinearEquivCochains N 0) (dgClosedHom R f))

    The underlying map is the cochain of the closed degree-zero component.

    source
    theorem TauCeti.CurvedDGRightModuleCat.closedHom_injective {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} :
    Function.Injective closedHom

    Closed morphisms are determined by their underlying right-linear maps.

    source
    theorem TauCeti.CurvedDGRightModuleCat.closedHom_ext {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 g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N} (hfg : โˆ€ (x : M.carrier), (closedHom f) x = (closedHom g) x) :
    f = g

    Closed morphisms are equal when their values agree.

    source
    theorem TauCeti.CurvedDGRightModuleCat.closedHom_ext_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 g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N} :
    f = g โ†” โˆ€ (x : M.carrier), (closedHom f) x = (closedHom g) x
    source
    noncomputable def TauCeti.CurvedDGRightModuleCat.closedHomOf {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 : M.carrier โ†’โ‚—[Aแตแต’แต–] N.carrier) (hf : โˆ€ (p : โ„ค), โˆ€ x โˆˆ M.grading p, f x โˆˆ N.grading p) (hd : โˆ€ (x : M.carrier), N.differential (f x) = f (M.differential x)) :
    CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N

    Construct a closed morphism from a graded right-linear map commuting with differentials.

    Instances For
      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedHomOf {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 : M.carrier โ†’โ‚—[Aแตแต’แต–] N.carrier) (hf : โˆ€ (p : โ„ค), โˆ€ x โˆˆ M.grading p, f x โˆˆ N.grading p) (hd : โˆ€ (x : M.carrier), N.differential (f x) = f (M.differential x)) :
      closedHom (closedHomOf f hf hd) = f

      The constructor retains its prescribed right-linear map.

      source
      theorem TauCeti.CurvedDGRightModuleCat.closedHom_mem {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 : M.carrier} (hx : x โˆˆ M.grading p) :
      (closedHom f) x โˆˆ N.grading p

      A closed morphism preserves homogeneous pieces.

      source
      theorem TauCeti.CurvedDGRightModuleCat.isHomogeneous_closedHom {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) :
      LinearMap.IsHomogeneous (โ†‘R (closedHom f)) M.grading N.grading 0

      The ground-ring linear map underlying a closed morphism is homogeneous of degree zero.

      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.differential_closedHom {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 : M.carrier) :
      N.differential ((closedHom f) x) = (closedHom f) (M.differential x)

      A closed morphism commutes with the differentials.

      source
      theorem TauCeti.CurvedDGRightModuleCat.differential_comp_closedHom {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.differential โˆ˜โ‚— โ†‘R (closedHom f) = โ†‘R (closedHom f) โˆ˜โ‚— M.differential

      The ground-ring linear map underlying a closed morphism commutes with the differentials.

      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.closedHom_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} (M : CurvedDGRightModuleCat h) :
      closedHom (CategoryTheory.CategoryStruct.id (CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M)) = LinearMap.id

      The identity closed morphism is the identity right-linear map.

      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.closedHom_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 P : CurvedDGRightModuleCat h} (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N) (g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) P) :
      closedHom (CategoryTheory.CategoryStruct.comp f g) = closedHom g โˆ˜โ‚— closedHom f

      Composition of closed morphisms is composition of right-linear maps.

      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.closedHom_zero {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) :
      closedHom 0 = 0

      The zero closed morphism has zero underlying linear map.

      source
      @[simp]
      theorem TauCeti.CurvedDGRightModuleCat.closedHom_add {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 g : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N) :
      closedHom (f + g) = closedHom f + closedHom g

      Addition of closed morphisms is addition of their underlying linear maps.

      source
      noncomputable def TauCeti.CurvedDGRightModuleCat.closedIsoOf {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} (e : M.carrier โ‰ƒโ‚—[Aแตแต’แต–] N.carrier) (he : โˆ€ (p : โ„ค) (x : M.carrier), x โˆˆ M.grading p โ†” e x โˆˆ N.grading p) (hd : โˆ€ (x : M.carrier), N.differential (e x) = e (M.differential x)) :
      CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โ‰… CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N

      A graded right-linear equivalence commuting with differentials is a closed isomorphism.

      Instances For
        source
        @[simp]
        theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedIsoOf_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} (e : M.carrier โ‰ƒโ‚—[Aแตแต’แต–] N.carrier) (he : โˆ€ (p : โ„ค) (x : M.carrier), x โˆˆ M.grading p โ†” e x โˆˆ N.grading p) (hd : โˆ€ (x : M.carrier), N.differential (e x) = e (M.differential x)) :
        closedHom (closedIsoOf e he hd).hom = โ†‘e

        The forward map of the closed isomorphism is the supplied equivalence.

        source
        @[simp]
        theorem TauCeti.CurvedDGRightModuleCat.closedHom_closedIsoOf_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} (e : M.carrier โ‰ƒโ‚—[Aแตแต’แต–] N.carrier) (he : โˆ€ (p : โ„ค) (x : M.carrier), x โˆˆ M.grading p โ†” e x โˆˆ N.grading p) (hd : โˆ€ (x : M.carrier), N.differential (e x) = e (M.differential x)) :
        closedHom (closedIsoOf e he hd).inv = โ†‘e.symm

        The inverse map of the closed isomorphism is the inverse equivalence.

        source
        @[simp]
        theorem TauCeti.CurvedDGRightModuleCat.closedHom_smul {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} (r : R) (f : CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) M โŸถ CategoryTheory.ForgetEnrichment.of (CochainComplex (ModuleCat R) โ„ค) N) :
        closedHom (r โ€ข f) = r โ€ข closedHom f

        Scalar multiplication of closed morphisms acts on their underlying right-linear maps.