The category of conflations

For a fixed conflation class E, a conflation is not merely a proposition about a short complex: conflations and commutative diagrams between them form a category. This file realizes that category as the full subcategory of ShortComplex C on the distinguished kernel--cokernel pairs. Consequently, a morphism of conflations is exactly a ladder of two commuting squares with three vertical maps, and an isomorphism of conflations is exactly such a ladder whose vertical maps are isomorphisms.

The construction deliberately reuses Mathlib's category of short complexes. In particular, composition, identities, the preadditive structure, component functors, and the componentwise criterion for isomorphisms are inherited rather than duplicated.

Conflation-exact functors induce functors between conflation categories. Naturally isomorphic conflation-exact functors induce naturally isomorphic functors, and passage to the opposite conflation class gives the expected equivalence on conflations.

Main definitions and results

• TauCeti.ConflationClass.ConflationCategory: the full subcategory of distinguished short complexes.
• TauCeti.ConflationClass.ConflationCategory.homMk and .isoMk: constructors for maps and isomorphisms of conflations from their three components.
• TauCeti.ConflationClass.ConflationCategory.isIso_iff: a map of conflations is an isomorphism exactly when all three components are isomorphisms.
• TauCeti.ConflationClass.ConflationCategory.map: the functor induced by a functor preserving conflations, with TauCeti.ExactStructure.ConflationCategory.map as its exact-structure specialization.
• TauCeti.ConflationClass.ConflationCategory.mapIdIso and .mapCompIso: identity and composition coherence for the induced functor.
• TauCeti.ConflationClass.ConflationCategory.mapNatIso: natural-isomorphism invariance of the induced functor.
• TauCeti.ConflationClass.ConflationCategory.opEquivalence: the equivalence E.ConflationCategoryᵒᵖ ≌ E.op.ConflationCategory.

References

• Theo Bühler, Exact categories, Expositiones Mathematicae 28 (2010), 1--69, https://arxiv.org/abs/0811.1480, Sections 2 and 5.

@[reducible, inline]

abbrev TauCeti.ConflationClass.ConflationCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : Type (max u₁ v₁)

The category of conflations of a conflation class E. Its objects are distinguished short complexes, and its morphisms are arbitrary morphisms of the underlying short complexes.

Equations

• E.ConflationCategory = CategoryTheory.ObjectProperty.FullSubcategory fun (S : CategoryTheory.ShortComplex C) => E.Conflation S

@[reducible, inline]

abbrev TauCeti.ConflationClass.ConflationCategory.ι {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : CategoryTheory.Functor E.ConflationCategory (CategoryTheory.ShortComplex C)

The fully faithful inclusion of the category of conflations into the category of short complexes.

Equations

• TauCeti.ConflationClass.ConflationCategory.ι E = CategoryTheory.ObjectProperty.ι fun (S : CategoryTheory.ShortComplex C) => E.Conflation S

@[reducible, inline]

abbrev TauCeti.ConflationClass.ConflationCategory.π₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : CategoryTheory.Functor E.ConflationCategory C

The left-object functor on the category of conflations.

Equations

• TauCeti.ConflationClass.ConflationCategory.π₁ E = (TauCeti.ConflationClass.ConflationCategory.ι E).comp CategoryTheory.ShortComplex.π₁

@[reducible, inline]

abbrev TauCeti.ConflationClass.ConflationCategory.π₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : CategoryTheory.Functor E.ConflationCategory C

The middle-object functor on the category of conflations.

Equations

• TauCeti.ConflationClass.ConflationCategory.π₂ E = (TauCeti.ConflationClass.ConflationCategory.ι E).comp CategoryTheory.ShortComplex.π₂

@[reducible, inline]

abbrev TauCeti.ConflationClass.ConflationCategory.π₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : CategoryTheory.Functor E.ConflationCategory C

The right-object functor on the category of conflations.

Equations

• TauCeti.ConflationClass.ConflationCategory.π₃ E = (TauCeti.ConflationClass.ConflationCategory.ι E).comp CategoryTheory.ShortComplex.π₃

@[reducible, inline]

abbrev TauCeti.ConflationClass.ConflationCategory.π₁Toπ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : π₁ E ⟶ π₂ E

The first arrow of every conflation, as a natural transformation.

Equations

• TauCeti.ConflationClass.ConflationCategory.π₁Toπ₂ E = (TauCeti.ConflationClass.ConflationCategory.ι E).whiskerLeft CategoryTheory.ShortComplex.π₁Toπ₂

@[reducible, inline]

abbrev TauCeti.ConflationClass.ConflationCategory.π₂Toπ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : π₂ E ⟶ π₃ E

The second arrow of every conflation, as a natural transformation.

Equations

• TauCeti.ConflationClass.ConflationCategory.π₂Toπ₃ E = (TauCeti.ConflationClass.ConflationCategory.ι E).whiskerLeft CategoryTheory.ShortComplex.π₂Toπ₃

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.π₁Toπ₂_comp_π₂Toπ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) : CategoryTheory.CategoryStruct.comp (π₁Toπ₂ E) (π₂Toπ₃ E) = 0

The composite of the natural transformations π₁Toπ₂ E and π₂Toπ₃ E between the component functors is zero.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.π₁Toπ₂_comp_π₂Toπ₃_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {Z : CategoryTheory.Functor E.ConflationCategory C} (h : π₃ E ⟶ Z) : CategoryTheory.CategoryStruct.comp (π₁Toπ₂ E) (CategoryTheory.CategoryStruct.comp (π₂Toπ₃ E) h) = CategoryTheory.CategoryStruct.comp 0 h

The composite of the natural transformations π₁Toπ₂ E and π₂Toπ₃ E between the component functors is zero.

instance TauCeti.ConflationClass.ConflationCategory.mono_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} (S : E.ConflationCategory) : CategoryTheory.Mono S.obj.f

The first arrow of a conflation is a monomorphism.

instance TauCeti.ConflationClass.ConflationCategory.epi_g {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} (S : E.ConflationCategory) : CategoryTheory.Epi S.obj.g

The second arrow of a conflation is an epimorphism.

def TauCeti.ConflationClass.ConflationCategory.homMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (τ₁ : S.obj.X₁ ⟶ T.obj.X₁) (τ₂ : S.obj.X₂ ⟶ T.obj.X₂) (τ₃ : S.obj.X₃ ⟶ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f τ₂ := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g τ₃ := by cat_disch) : S ⟶ T

Construct a morphism of conflations from three maps making the two squares commute.

Equations

• TauCeti.ConflationClass.ConflationCategory.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃ = CategoryTheory.ObjectProperty.homMk (CategoryTheory.ShortComplex.homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃)

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.homMk_hom_τ₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (τ₁ : S.obj.X₁ ⟶ T.obj.X₁) (τ₂ : S.obj.X₂ ⟶ T.obj.X₂) (τ₃ : S.obj.X₃ ⟶ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f τ₂ := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g τ₃ := by cat_disch) : (homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).hom.τ₁ = τ₁

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.homMk_hom_τ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (τ₁ : S.obj.X₁ ⟶ T.obj.X₁) (τ₂ : S.obj.X₂ ⟶ T.obj.X₂) (τ₃ : S.obj.X₃ ⟶ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f τ₂ := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g τ₃ := by cat_disch) : (homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).hom.τ₂ = τ₂

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.homMk_hom_τ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (τ₁ : S.obj.X₁ ⟶ T.obj.X₁) (τ₂ : S.obj.X₂ ⟶ T.obj.X₂) (τ₃ : S.obj.X₃ ⟶ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp τ₁ T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f τ₂ := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp τ₂ T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g τ₃ := by cat_disch) : (homMk τ₁ τ₂ τ₃ comm₁₂ comm₂₃).hom.τ₃ = τ₃

def TauCeti.ConflationClass.ConflationCategory.isoMk {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (e₁ : S.obj.X₁ ≅ T.obj.X₁) (e₂ : S.obj.X₂ ≅ T.obj.X₂) (e₃ : S.obj.X₃ ≅ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f e₂.hom := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g e₃.hom := by cat_disch) : S ≅ T

Construct an isomorphism of conflations from compatible isomorphisms of the three terms.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.isoMk_hom_hom_τ₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (e₁ : S.obj.X₁ ≅ T.obj.X₁) (e₂ : S.obj.X₂ ≅ T.obj.X₂) (e₃ : S.obj.X₃ ≅ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f e₂.hom := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g e₃.hom := by cat_disch) : (isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.hom.τ₁ = e₁.hom

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.isoMk_hom_hom_τ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (e₁ : S.obj.X₁ ≅ T.obj.X₁) (e₂ : S.obj.X₂ ≅ T.obj.X₂) (e₃ : S.obj.X₃ ≅ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f e₂.hom := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g e₃.hom := by cat_disch) : (isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.hom.τ₂ = e₂.hom

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.isoMk_hom_hom_τ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (e₁ : S.obj.X₁ ≅ T.obj.X₁) (e₂ : S.obj.X₂ ≅ T.obj.X₂) (e₃ : S.obj.X₃ ≅ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f e₂.hom := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g e₃.hom := by cat_disch) : (isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).hom.hom.τ₃ = e₃.hom

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.isoMk_inv_hom_τ₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (e₁ : S.obj.X₁ ≅ T.obj.X₁) (e₂ : S.obj.X₂ ≅ T.obj.X₂) (e₃ : S.obj.X₃ ≅ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f e₂.hom := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g e₃.hom := by cat_disch) : (isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).inv.hom.τ₁ = e₁.inv

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.isoMk_inv_hom_τ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (e₁ : S.obj.X₁ ≅ T.obj.X₁) (e₂ : S.obj.X₂ ≅ T.obj.X₂) (e₃ : S.obj.X₃ ≅ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f e₂.hom := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g e₃.hom := by cat_disch) : (isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).inv.hom.τ₂ = e₂.inv

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.isoMk_inv_hom_τ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (e₁ : S.obj.X₁ ≅ T.obj.X₁) (e₂ : S.obj.X₂ ≅ T.obj.X₂) (e₃ : S.obj.X₃ ≅ T.obj.X₃) (comm₁₂ : CategoryTheory.CategoryStruct.comp e₁.hom T.obj.f = CategoryTheory.CategoryStruct.comp S.obj.f e₂.hom := by cat_disch) (comm₂₃ : CategoryTheory.CategoryStruct.comp e₂.hom T.obj.g = CategoryTheory.CategoryStruct.comp S.obj.g e₃.hom := by cat_disch) : (isoMk e₁ e₂ e₃ comm₁₂ comm₂₃).inv.hom.τ₃ = e₃.inv

theorem TauCeti.ConflationClass.ConflationCategory.isIso_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {S T : E.ConflationCategory} (a : S ⟶ T) : CategoryTheory.IsIso a ↔ CategoryTheory.IsIso a.hom.τ₁ ∧ CategoryTheory.IsIso a.hom.τ₂ ∧ CategoryTheory.IsIso a.hom.τ₃

A morphism of conflations is an isomorphism exactly when its three components are isomorphisms.

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

Taking opposites gives an equivalence from the opposite of the category of conflations to the category of conflations of the opposite conflation class.

Equations

• TauCeti.ConflationClass.ConflationCategory.opEquivalence E = E.Conflation.opEquivalence.symm.trans ((CategoryTheory.ShortComplex.opEquiv C).congrFullSubcategory ⋯)

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_functor_obj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) (S : E.ConflationCategoryᵒᵖ) : ((opEquivalence E).functor.obj S).obj = (Opposite.unop S).obj.op

The underlying short complex of the opposite of a conflation is S.unop.obj.op: its arrows are S.unop.obj.g.op and S.unop.obj.f.op, so its outer terms are exchanged.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_inverse_obj_unop_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) (S : E.op.ConflationCategory) : (Opposite.unop ((opEquivalence E).inverse.obj S)).obj = S.obj.unop

The underlying short complex obtained by unopposing a conflation reverses the opposite short complex again, exchanging its outer terms.

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_functor_map_hom_heq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : E.ConflationCategoryᵒᵖ} (a : S ⟶ T) : ((opEquivalence E).functor.map a).hom ≍ CategoryTheory.ShortComplex.opMap a.unop.hom

On morphisms, taking opposites applies ShortComplex.opMap, which reverses direction and sends τ₁ to τ₃.op.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_functor_map_hom_τ₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : E.ConflationCategoryᵒᵖ} (a : S ⟶ T) : ((opEquivalence E).functor.map a).hom.τ₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp a.unop.hom.τ₃.op (CategoryTheory.eqToHom ⋯))

On the first component, taking opposites reverses direction and sends τ₁ to τ₃.op.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_functor_map_hom_τ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : E.ConflationCategoryᵒᵖ} (a : S ⟶ T) : ((opEquivalence E).functor.map a).hom.τ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp a.unop.hom.τ₂.op (CategoryTheory.eqToHom ⋯))

On the middle component, taking opposites sends τ₂ to τ₂.op.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_functor_map_hom_τ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : E.ConflationCategoryᵒᵖ} (a : S ⟶ T) : ((opEquivalence E).functor.map a).hom.τ₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp a.unop.hom.τ₁.op (CategoryTheory.eqToHom ⋯))

On the third component, taking opposites reverses direction and sends τ₃ to τ₁.op.

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_inverse_map_unop_hom_heq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : E.op.ConflationCategory} (a : S ⟶ T) : ((opEquivalence E).inverse.map a).unop.hom ≍ CategoryTheory.ShortComplex.unopMap a.hom

On morphisms, unopposing applies ShortComplex.unopMap, which reverses direction and sends τ₁ to τ₃.unop.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_inverse_map_unop_hom_τ₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : E.op.ConflationCategory} (a : S ⟶ T) : ((opEquivalence E).inverse.map a).unop.hom.τ₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp a.hom.τ₃.unop (CategoryTheory.eqToHom ⋯))

On the first component, unopposing reverses direction and sends τ₁ to τ₃.unop.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_inverse_map_unop_hom_τ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : E.op.ConflationCategory} (a : S ⟶ T) : ((opEquivalence E).inverse.map a).unop.hom.τ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp a.hom.τ₂.unop (CategoryTheory.eqToHom ⋯))

On the middle component, unopposing sends τ₂ to τ₂.unop.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.opEquivalence_inverse_map_unop_hom_τ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] (E : ConflationClass C) {S T : E.op.ConflationCategory} (a : S ⟶ T) : ((opEquivalence E).inverse.map a).unop.hom.τ₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp a.hom.τ₁.unop (CategoryTheory.eqToHom ⋯))

On the third component, unopposing reverses direction and sends τ₃ to τ₁.unop.

def TauCeti.ConflationClass.ConflationCategory.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) : CategoryTheory.Functor E.ConflationCategory E'.ConflationCategory

A functor preserving zero morphisms and conflations induces a functor between the corresponding categories of conflations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.map_obj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (S : E.ConflationCategory) : ((map F ⋯).obj S).obj = F.mapShortComplex.obj S.obj

The underlying short complex of a mapped conflation is its componentwise image.

theorem TauCeti.ConflationClass.ConflationCategory.map_obj_obj_X₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (S : E.ConflationCategory) : ((map F ⋯).obj S).obj.X₁ = F.obj S.obj.X₁

theorem TauCeti.ConflationClass.ConflationCategory.map_obj_obj_X₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (S : E.ConflationCategory) : ((map F ⋯).obj S).obj.X₂ = F.obj S.obj.X₂

theorem TauCeti.ConflationClass.ConflationCategory.map_obj_obj_X₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (S : E.ConflationCategory) : ((map F ⋯).obj S).obj.X₃ = F.obj S.obj.X₃

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.map_obj_obj_f {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (S : E.ConflationCategory) : ((map F ⋯).obj S).obj.f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F.map S.obj.f) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.map_obj_obj_g {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (S : E.ConflationCategory) : ((map F ⋯).obj S).obj.g = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F.map S.obj.g) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.map_map_hom_τ₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) {S T : E.ConflationCategory} (a : S ⟶ T) : ((map F ⋯).map a).hom.τ₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F.map a.hom.τ₁) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.map_map_hom_τ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) {S T : E.ConflationCategory} (a : S ⟶ T) : ((map F ⋯).map a).hom.τ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F.map a.hom.τ₂) (CategoryTheory.eqToHom ⋯))

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.map_map_hom_τ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) {S T : E.ConflationCategory} (a : S ⟶ T) : ((map F ⋯).map a).hom.τ₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (F.map a.hom.τ₃) (CategoryTheory.eqToHom ⋯))

def TauCeti.ConflationClass.ConflationCategory.mapCompιIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) : (map F ⋯).comp (ι E') ≅ (ι E).comp F.mapShortComplex

After forgetting that its objects are conflations, the induced functor is the ordinary componentwise map on short complexes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapCompιIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (S : E.ConflationCategory) : (mapCompιIso F ⋯).hom.app S = CategoryTheory.eqToHom ⋯

The forward component of mapCompιIso is the equality transport from the lifted object to its componentwise image.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapCompιIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (S : E.ConflationCategory) : (mapCompιIso F ⋯).inv.app S = CategoryTheory.eqToHom ⋯

The inverse component of mapCompιIso is the reverse equality transport.

def TauCeti.ConflationClass.ConflationCategory.mapIdIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} : map (CategoryTheory.Functor.id C) ⋯ ≅ CategoryTheory.Functor.id E.ConflationCategory

The functor on conflations induced by the identity functor is naturally isomorphic to the identity functor.

Equations

• TauCeti.ConflationClass.ConflationCategory.mapIdIso = CategoryTheory.Iso.refl (TauCeti.ConflationClass.ConflationCategory.map (CategoryTheory.Functor.id C) ⋯)

theorem TauCeti.ConflationClass.ConflationCategory.map_id_obj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} (S : E.ConflationCategory) : ((map (CategoryTheory.Functor.id C) ⋯).obj S).obj = S.obj

The mapped underlying short complex for the identity functor is the original short complex.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapIdIso_hom_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} (S : E.ConflationCategory) : (mapIdIso.hom.app S).hom = CategoryTheory.eqToHom ⋯

The forward component of mapIdIso is the equality transport to the original short complex.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapIdIso_inv_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} (S : E.ConflationCategory) : (mapIdIso.inv.app S).hom = CategoryTheory.eqToHom ⋯

The inverse component of mapIdIso is the reverse equality transport.

def TauCeti.ConflationClass.ConflationCategory.mapCompIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [CategoryTheory.Preadditive K] {E'' : ConflationClass K} (F : CategoryTheory.Functor C D) (H : CategoryTheory.Functor D K) [F.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hH : ∀ {S : CategoryTheory.ShortComplex D}, E'.Conflation S → E''.Conflation (S.map H)) : map (F.comp H) ⋯ ≅ (map F ⋯).comp (map H ⋯)

Mapping conflations by a composite is naturally isomorphic to mapping successively.

Equations

• TauCeti.ConflationClass.ConflationCategory.mapCompIso F H hF hH = CategoryTheory.Iso.refl (TauCeti.ConflationClass.ConflationCategory.map (F.comp H) ⋯)

theorem TauCeti.ConflationClass.ConflationCategory.map_comp_obj_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [CategoryTheory.Preadditive K] {E'' : ConflationClass K} (F : CategoryTheory.Functor C D) (H : CategoryTheory.Functor D K) [F.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hH : ∀ {S : CategoryTheory.ShortComplex D}, E'.Conflation S → E''.Conflation (S.map H)) (S : E.ConflationCategory) : ((map (F.comp H) ⋯).obj S).obj = (((map F ⋯).comp (map H ⋯)).obj S).obj

Mapping an underlying short complex by a composite agrees with mapping it successively.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapCompIso_hom_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [CategoryTheory.Preadditive K] {E'' : ConflationClass K} (F : CategoryTheory.Functor C D) (H : CategoryTheory.Functor D K) [F.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hH : ∀ {S : CategoryTheory.ShortComplex D}, E'.Conflation S → E''.Conflation (S.map H)) (S : E.ConflationCategory) : ((mapCompIso F H ⋯ ⋯).hom.app S).hom = CategoryTheory.eqToHom ⋯

The forward component of mapCompIso is the equality transport between the two mapped short complexes.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapCompIso_inv_app_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [CategoryTheory.Preadditive K] {E'' : ConflationClass K} (F : CategoryTheory.Functor C D) (H : CategoryTheory.Functor D K) [F.PreservesZeroMorphisms] [H.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hH : ∀ {S : CategoryTheory.ShortComplex D}, E'.Conflation S → E''.Conflation (S.map H)) (S : E.ConflationCategory) : ((mapCompIso F H ⋯ ⋯).inv.app S).hom = CategoryTheory.eqToHom ⋯

The inverse component of mapCompIso is the reverse equality transport.

def TauCeti.ConflationClass.ConflationCategory.mapNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F G : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hG : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map G)) (e : F ≅ G) : map F ⋯ ≅ map G ⋯

A natural isomorphism between functors preserving conflations induces a natural isomorphism between their functors on conflations.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapNatIso_hom_app_hom_τ₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F G : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hG : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map G)) (e : F ≅ G) (S : E.ConflationCategory) : ((mapNatIso F G ⋯ ⋯ e).hom.app S).hom.τ₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (e.hom.app S.obj.X₁) (CategoryTheory.eqToHom ⋯))

The τ₁ component of (mapNatIso F G hF hG e).hom at S is e.hom at S.obj.X₁, transported along the identifications map_obj_obj_X₁ for F and G.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapNatIso_hom_app_hom_τ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F G : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hG : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map G)) (e : F ≅ G) (S : E.ConflationCategory) : ((mapNatIso F G ⋯ ⋯ e).hom.app S).hom.τ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (e.hom.app S.obj.X₂) (CategoryTheory.eqToHom ⋯))

The τ₂ component of (mapNatIso F G hF hG e).hom at S is e.hom at S.obj.X₂, transported along the identifications map_obj_obj_X₂ for F and G.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapNatIso_hom_app_hom_τ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F G : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hG : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map G)) (e : F ≅ G) (S : E.ConflationCategory) : ((mapNatIso F G ⋯ ⋯ e).hom.app S).hom.τ₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (e.hom.app S.obj.X₃) (CategoryTheory.eqToHom ⋯))

The τ₃ component of (mapNatIso F G hF hG e).hom at S is e.hom at S.obj.X₃, transported along the identifications map_obj_obj_X₃ for F and G.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapNatIso_inv_app_hom_τ₁ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F G : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hG : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map G)) (e : F ≅ G) (S : E.ConflationCategory) : ((mapNatIso F G ⋯ ⋯ e).inv.app S).hom.τ₁ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (e.inv.app S.obj.X₁) (CategoryTheory.eqToHom ⋯))

The τ₁ component of (mapNatIso F G hF hG e).inv at S is e.inv at S.obj.X₁, transported along the identifications map_obj_obj_X₁ for G and F.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapNatIso_inv_app_hom_τ₂ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F G : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hG : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map G)) (e : F ≅ G) (S : E.ConflationCategory) : ((mapNatIso F G ⋯ ⋯ e).inv.app S).hom.τ₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (e.inv.app S.obj.X₂) (CategoryTheory.eqToHom ⋯))

The τ₂ component of (mapNatIso F G hF hG e).inv at S is e.inv at S.obj.X₂, transported along the identifications map_obj_obj_X₂ for G and F.

@[simp]

theorem TauCeti.ConflationClass.ConflationCategory.mapNatIso_inv_app_hom_τ₃ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {E : ConflationClass C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] {E' : ConflationClass D} (F G : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (hF : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map F)) (hG : ∀ {S : CategoryTheory.ShortComplex C}, E.Conflation S → E'.Conflation (S.map G)) (e : F ≅ G) (S : E.ConflationCategory) : ((mapNatIso F G ⋯ ⋯ e).inv.app S).hom.τ₃ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (e.inv.app S.obj.X₃) (CategoryTheory.eqToHom ⋯))

The τ₃ component of (mapNatIso F G hF hG e).inv at S is e.inv at S.obj.X₃, transported along the identifications map_obj_obj_X₃ for G and F.

@[reducible, inline]

abbrev TauCeti.ExactStructure.ConflationCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] (E : ExactStructure C) : Type (max u₁ v₁)

The category of conflations of an exact structure.

Equations

• E.ConflationCategory = E.ConflationCategory

@[reducible, inline]

abbrev TauCeti.ExactStructure.ConflationCategory.map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) : CategoryTheory.Functor E.ConflationCategory E'.ConflationCategory

A conflation-exact functor induces a functor between the corresponding categories of conflations.

Equations

• TauCeti.ExactStructure.ConflationCategory.map hF = TauCeti.ConflationClass.ConflationCategory.map F ⋯

@[reducible, inline]

abbrev TauCeti.ExactStructure.ConflationCategory.mapCompιIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : E.IsConflationExact E' F) : (map hF).comp (ConflationClass.ConflationCategory.ι E'.toConflationClass) ≅ (ConflationClass.ConflationCategory.ι E.toConflationClass).comp F.mapShortComplex

After forgetting that its objects are conflations, the induced functor is the ordinary componentwise map on short complexes.

Equations

• TauCeti.ExactStructure.ConflationCategory.mapCompιIso hF = TauCeti.ConflationClass.ConflationCategory.mapCompιIso F ⋯

@[reducible, inline]

abbrev TauCeti.ExactStructure.ConflationCategory.mapIdIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} : map ⋯ ≅ CategoryTheory.Functor.id E.ConflationCategory

The functor on conflations induced by the identity functor is naturally isomorphic to the identity functor.

Equations

• TauCeti.ExactStructure.ConflationCategory.mapIdIso = TauCeti.ConflationClass.ConflationCategory.mapIdIso

@[reducible, inline]

abbrev TauCeti.ExactStructure.ConflationCategory.mapCompIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {F : CategoryTheory.Functor C D} {K : Type u_1} [CategoryTheory.Category.{v_1, u_1} K] [CategoryTheory.Preadditive K] [CategoryTheory.Limits.HasZeroObject K] [CategoryTheory.Limits.HasBinaryBiproducts K] {E'' : ExactStructure K} {H : CategoryTheory.Functor D K} [F.Additive] [H.Additive] (hF : E.IsConflationExact E' F) (hH : E'.IsConflationExact E'' H) : map ⋯ ≅ (map hF).comp (map hH)

Mapping conflations by a composite is naturally isomorphic to mapping successively.

Equations

• TauCeti.ExactStructure.ConflationCategory.mapCompIso hF hH = TauCeti.ConflationClass.ConflationCategory.mapCompIso F H ⋯ ⋯

@[reducible, inline]

abbrev TauCeti.ExactStructure.ConflationCategory.mapNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] {E : ExactStructure C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E' : ExactStructure D} {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (hF : E.IsConflationExact E' F) (hG : E.IsConflationExact E' G) (e : F ≅ G) : map hF ≅ map hG

A natural isomorphism between conflation-exact functors induces a natural isomorphism between their functors on conflations.

Equations

• TauCeti.ExactStructure.ConflationCategory.mapNatIso hF hG e = TauCeti.ConflationClass.ConflationCategory.mapNatIso F G ⋯ ⋯ e