Documentation

TauCeti.CategoryTheory.Exact.Equivalence

Transporting exact structures along equivalences #

An additive equivalence transports a Quillen exact structure to its target. A short complex in the target is distinguished precisely when its image under the inverse equivalence is distinguished. This file verifies all six exact-category axioms for that transported class and shows that both functors of the equivalence preserve and reflect conflations.

Main definitions and results #

References #

source
noncomputable def TauCeti.ExactStructure.transport {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] :
ExactStructure D

Transport an exact structure along an additive equivalence. The distinguished short complexes in the target are those whose images under the inverse equivalence are distinguished in the source.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.ExactStructure.transport_conflation_iff {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] (S : CategoryTheory.ShortComplex D) :
    (E.transport e).Conflation S ↔ E.Conflation (S.map e.inverse)

    A short complex is a conflation in the transported exact structure exactly when its image under the inverse equivalence is a conflation in the source.

    source
    theorem TauCeti.ExactStructure.transport_inflations {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] :
    (E.transport e).inflations = E.inflations.inverseImage e.inverse

    The inflations of the transported exact structure are the morphisms whose images under the inverse equivalence are inflations.

    source
    theorem TauCeti.ExactStructure.transport_deflations {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] :
    (E.transport e).deflations = E.deflations.inverseImage e.inverse

    The deflations of the transported exact structure are the morphisms whose images under the inverse equivalence are deflations.

    source
    @[simp]
    theorem TauCeti.ExactStructure.transport_isInflation_iff {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] {X Y : D} (i : X ⟶ Y) :
    (E.transport e).IsInflation i ↔ E.IsInflation (e.inverse.map i)

    A morphism is an inflation for the transported exact structure exactly when its image under the inverse equivalence is an inflation.

    source
    @[simp]
    theorem TauCeti.ExactStructure.transport_isDeflation_iff {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] {Y Z : D} (p : Y ⟶ Z) :
    (E.transport e).IsDeflation p ↔ E.IsDeflation (e.inverse.map p)

    A morphism is a deflation for the transported exact structure exactly when its image under the inverse equivalence is a deflation.

    source
    theorem TauCeti.ExactStructure.isConflationExact_functor_transport {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] :
    E.IsConflationExact (E.transport e) e.functor

    The forward functor of an additive equivalence is conflation-exact from an exact structure to its transport.

    source
    theorem TauCeti.ExactStructure.reflectsConflations_functor_transport {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] :
    E.ReflectsConflations (E.transport e) e.functor

    The forward functor of an additive equivalence reflects the conflations of a transported exact structure.

    source
    theorem TauCeti.ExactStructure.isConflationExact_inverse_transport {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] :
    (E.transport e).IsConflationExact E e.inverse

    The inverse functor of an additive equivalence is conflation-exact from the transported exact structure back to the source.

    source
    theorem TauCeti.ExactStructure.reflectsConflations_inverse_transport {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] :
    (E.transport e).ReflectsConflations E e.inverse

    The inverse functor of an additive equivalence reflects source conflations back to the transported exact structure.

    source
    @[simp]
    theorem TauCeti.ExactStructure.transport_symm {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : ExactStructure C) (e : C ≌ D) [e.functor.Additive] :
    (E.transport e).transport e.symm = E

    Transporting an exact structure along an equivalence and then along its inverse recovers the original exact structure.

    source
    theorem TauCeti.ExactStructure.reflectsConflations_of_isConflationExact_inverse {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} (e : C ≌ D) [e.functor.Additive] (hG : E'.IsConflationExact E e.inverse) :
    E.ReflectsConflations E' e.functor

    An additive equivalence whose inverse is conflation-exact reflects conflations.

    source
    theorem TauCeti.ExactStructure.isConflationExact_inverse_of_reflectsConflations {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} (e : C ≌ D) [e.functor.Additive] (hR : E.ReflectsConflations E' e.functor) :
    E'.IsConflationExact E e.inverse

    An additive equivalence which reflects conflations has a conflation-exact inverse. No exactness of the equivalence itself is used.

    source
    theorem TauCeti.ExactStructure.isConflationExact_inverse_iff_reflectsConflations {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} (e : C ≌ D) [e.functor.Additive] :
    E'.IsConflationExact E e.inverse ↔ E.ReflectsConflations E' e.functor

    For an additive equivalence, conflation-exactness of the inverse and reflection of conflations are the same condition.