Documentation

TauCeti.CategoryTheory.Exact.Opposite

Opposite exact structures #

Every exact structure on an additive category induces an exact structure on the opposite category. Its conflations are the opposites of the original conflations, so its inflations are the opposites of the original deflations and its deflations are the opposites of the original inflations.

This file develops the self-duality of the intrinsic Quillen axioms. Identity and composition exchange their inflation and deflation forms, while pullbacks of deflations become pushouts of inflations and conversely.

Main definitions #

Main results #

References #

source
def TauCeti.ConflationClass.op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) :
ConflationClass Cᵒᵖ

The opposite of a conflation class. A short complex in Cᵒᵖ is distinguished exactly when its un-opposite is distinguished in C.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.ConflationClass.op_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) (S : CategoryTheory.ShortComplex Cᵒᵖ) :
    E.op.Conflation S ↔ E.Conflation S.unop

    A short complex is a conflation of the opposite class exactly when its un-opposite is a conflation of the original class.

    source
    theorem TauCeti.ConflationClass.op_conflation_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) (S : CategoryTheory.ShortComplex C) :
    E.op.Conflation S.op ↔ E.Conflation S

    Opposite conflations are precisely the opposites of the original conflations.

    This is not a simp lemma: op_conflation already rewrites the left-hand side, to the definitionally equal E.Conflation S.op.unop.

    source
    theorem TauCeti.ConflationClass.op_conflation_inverseImage {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) :
    E.op.Conflation.inverseImage (CategoryTheory.ShortComplex.opEquiv C).functor = E.Conflation.op

    The inverse image of opposite conflations under the short-complex opposite equivalence is the opposite of the original conflation property.

    source
    theorem TauCeti.ConflationClass.op_inflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) :
    E.op.inflations = E.deflations.op

    The inflations of the opposite conflation class are the opposites of its deflations.

    source
    theorem TauCeti.ConflationClass.op_deflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) :
    E.op.deflations = E.inflations.op

    The deflations of the opposite conflation class are the opposites of its inflations.

    source
    @[simp]
    theorem TauCeti.ConflationClass.op_isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    E.op.IsInflation f ↔ E.IsDeflation f.unop

    A morphism is an inflation in the opposite conflation class exactly when its un-opposite is a deflation in the original class.

    source
    @[simp]
    theorem TauCeti.ConflationClass.op_isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    E.op.IsDeflation f ↔ E.IsInflation f.unop

    A morphism is a deflation in the opposite conflation class exactly when its un-opposite is an inflation in the original class.

    source
    noncomputable def TauCeti.ExactStructure.op {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :
    ExactStructure Cᵒᵖ

    The opposite exact structure. Its conflations are the short complexes whose un-opposites are conflations of the original exact structure.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.ExactStructure.op_conflation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (S : CategoryTheory.ShortComplex Cᵒᵖ) :
      E.op.Conflation S ↔ E.Conflation S.unop

      A short complex is a conflation of the opposite exact structure exactly when its un-opposite is a conflation of the original exact structure.

      source
      theorem TauCeti.ExactStructure.op_conflation_op_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) (S : CategoryTheory.ShortComplex C) :
      E.op.Conflation S.op ↔ E.Conflation S

      The opposite of a conflation is a conflation in the opposite exact structure, and every such opposite conflation arises this way.

      This is not a simp lemma: op_conflation already rewrites the left-hand side, to the definitionally equal E.Conflation S.op.unop.

      source
      theorem TauCeti.ExactStructure.op_inflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :
      E.op.inflations = E.deflations.op

      The inflations of the opposite exact structure are the opposites of the original deflations.

      source
      theorem TauCeti.ExactStructure.op_deflations {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) :
      E.op.deflations = E.inflations.op

      The deflations of the opposite exact structure are the opposites of the original inflations.

      source
      @[simp]
      theorem TauCeti.ExactStructure.op_isInflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
      E.op.IsInflation f ↔ E.IsDeflation f.unop

      A morphism is an inflation of the opposite exact structure exactly when its un-opposite is a deflation of the original exact structure.

      source
      @[simp]
      theorem TauCeti.ExactStructure.op_isDeflation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
      E.op.IsDeflation f ↔ E.IsInflation f.unop

      A morphism is a deflation of the opposite exact structure exactly when its un-opposite is an inflation of the original exact structure.