Documentation

TauCeti.CategoryTheory.Exact.Product

Products of exact categories #

The product of two exact categories carries the componentwise exact structure: a short complex in the product is a conflation precisely when both of its projections are conflations. This file constructs that exact structure directly from Quillen's axioms and records its characteristic lemmas.

The projection functors preserve conflations and jointly detect them. Inserting a zero object in either coordinate is also conflation-exact. These functors are the input for the product formula for exact Grothendieck groups. Relative projectives and injectives are computed componentwise, and products preserve enough projectives, enough injectives, and Frobenius exact structures. This also supplies the exact structure used to compare stable categories with their products.

Main definitions #

Main results #

References #

source
theorem TauCeti.instPreservesZeroMorphismsProdFst_tauCeti {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] :
(CategoryTheory.Prod.fst C D).PreservesZeroMorphisms
source
theorem TauCeti.instPreservesZeroMorphismsProdSnd_tauCeti {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] :
(CategoryTheory.Prod.snd C D).PreservesZeroMorphisms
source
theorem TauCeti.isKernelCokernelPair_prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex (C × D)) (h₁ : IsKernelCokernelPair (S.map (CategoryTheory.Prod.fst C D))) (h₂ : IsKernelCokernelPair (S.map (CategoryTheory.Prod.snd C D))) :
IsKernelCokernelPair S

In a product of categories with zero morphisms, a short complex whose two projections are kernel–cokernel pairs is a kernel–cokernel pair: kernels and cokernels are computed componentwise.

source
noncomputable def TauCeti.ExactStructure.prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) :
ExactStructure (C × D)

The componentwise exact structure on a product category. A short complex is a conflation when each of its two projections is a conflation.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.ExactStructure.prod_isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) {X Y : C × D} (i : X ⟶ Y) :
    (E.prod E').IsInflation i ↔ E.IsInflation i.1 ∧ E'.IsInflation i.2

    A morphism is an inflation for the product exact structure exactly when both components are inflations.

    source
    @[simp]
    theorem TauCeti.ExactStructure.prod_isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) {Y Z : C × D} (p : Y ⟶ Z) :
    (E.prod E').IsDeflation p ↔ E.IsDeflation p.1 ∧ E'.IsDeflation p.2

    A morphism is a deflation for the product exact structure exactly when both components are deflations.

    source
    @[simp]
    theorem TauCeti.ExactStructure.prod_conflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (S : CategoryTheory.ShortComplex (C × D)) :
    (E.prod E').Conflation S ↔ E.Conflation (S.map (CategoryTheory.Prod.fst C D)) ∧ E'.Conflation (S.map (CategoryTheory.Prod.snd C D))

    A short complex is a conflation for the product exact structure exactly when both projected short complexes are conflations.

    source
    theorem TauCeti.ExactStructure.isConflationExact_fst_prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) :
    (E.prod E').IsConflationExact E (CategoryTheory.Prod.fst C D)

    The first projection from a product exact category preserves conflations.

    source
    theorem TauCeti.ExactStructure.isConflationExact_snd_prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) :
    (E.prod E').IsConflationExact E' (CategoryTheory.Prod.snd C D)

    The second projection from a product exact category preserves conflations.

    source
    theorem TauCeti.ExactStructure.isConflationExact_sectL_prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) :
    E.IsConflationExact (E.prod E') (CategoryTheory.Prod.sectL C 0)

    Inserting a zero object in the second coordinate preserves conflations.

    source
    theorem TauCeti.ExactStructure.isConflationExact_sectR_prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) :
    E'.IsConflationExact (E.prod E') (CategoryTheory.Prod.sectR 0 D)

    Inserting a zero object in the first coordinate preserves conflations.

    source
    theorem TauCeti.ExactStructure.IsConflationExact.prod {C₁ : Type u} [CategoryTheory.Category.{v, u} C₁] [CategoryTheory.Preadditive C₁] [CategoryTheory.Limits.HasZeroObject C₁] [CategoryTheory.Limits.HasBinaryBiproducts C₁] {C₂ : Type u_1} [CategoryTheory.Category.{u_3, u_1} C₂] [CategoryTheory.Preadditive C₂] [CategoryTheory.Limits.HasZeroObject C₂] [CategoryTheory.Limits.HasBinaryBiproducts C₂] {D₁ : Type u'} [CategoryTheory.Category.{v', u'} D₁] [CategoryTheory.Preadditive D₁] [CategoryTheory.Limits.HasZeroObject D₁] [CategoryTheory.Limits.HasBinaryBiproducts D₁] {D₂ : Type u_2} [CategoryTheory.Category.{u_4, u_2} D₂] [CategoryTheory.Preadditive D₂] [CategoryTheory.Limits.HasZeroObject D₂] [CategoryTheory.Limits.HasBinaryBiproducts D₂] {E₁ : ExactStructure C₁} {E₂ : ExactStructure C₂} {E₁' : ExactStructure D₁} {E₂' : ExactStructure D₂} {F : CategoryTheory.Functor C₁ C₂} {G : CategoryTheory.Functor D₁ D₂} [F.Additive] [G.Additive] (hF : E₁.IsConflationExact E₂ F) (hG : E₁'.IsConflationExact E₂' G) :
    (E₁.prod E₁').IsConflationExact (E₂.prod E₂') (F.prod G)

    The product of two conflation-exact functors is conflation-exact for the componentwise exact structures.

    source
    @[simp]
    theorem TauCeti.ExactStructure.prod_isProjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (Q : C × D) :
    (E.prod E').isProjective Q ↔ E.isProjective Q.1 ∧ E'.isProjective Q.2

    Relative projectivity for the product exact structure is componentwise.

    source
    @[simp]
    theorem TauCeti.ExactStructure.prod_isInjective_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (E' : ExactStructure D) (Q : C × D) :
    (E.prod E').isInjective Q ↔ E.isInjective Q.1 ∧ E'.isInjective Q.2

    Relative injectivity for the product exact structure is componentwise.

    source
    theorem TauCeti.ExactStructure.EnoughProjectives.prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} (hE : E.EnoughProjectives) (hE' : E'.EnoughProjectives) :
    (E.prod E').EnoughProjectives

    A product of exact categories with enough relative projectives has enough relative projectives, using componentwise presentations.

    source
    theorem TauCeti.ExactStructure.EnoughInjectives.prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} (hE : E.EnoughInjectives) (hE' : E'.EnoughInjectives) :
    (E.prod E').EnoughInjectives

    A product of exact categories with enough relative injectives has enough relative injectives, using componentwise presentations.

    source
    theorem TauCeti.ExactStructure.IsFrobenius.prod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) :
    (E.prod E').IsFrobenius

    The componentwise exact structure on a product of Frobenius exact categories is Frobenius. Its projective-injectives are the pairs of projective-injectives.