Normalizing the first map of a triangle-valued functor

Let T : J ⥤ Triangle C be a natural family of triangles. Applications often identify its first two projected functors with more meaningful functors F and G, and identify the transported first map with a named natural transformation α : F ⟶ G.

Triangle.FirstMapNormalizationData packages exactly those two endpoint isomorphisms and the required square. It constructs a new triangle-valued functor whose first two vertices and first map are literally F, G, and α, while leaving the third projected functor unchanged. Mathlib's Triangle.functorMk and Triangle.functorIsoMk supply the construction and its natural comparison with T.

This is an ordinary categorical interface. It does not assert that the triangles are distinguished, make any vertex functor exact, or make the normalization canonical. If the values of T are distinguished, the final theorem transports that pointwise fact to the normalized family.

For two normalizations with the same named first two vertices and first map, FirstMapNormalizationData.ComparisonData stores only a natural isomorphism of their third vertices and compatibility with the remaining two maps. It then delegates the full triangle-family isomorphism to Mathlib's Triangle.functorIsoMk'.

structure CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] (T : Functor J (Triangle C)) (F G : Functor J C) (α : F ⟶ G) : Type (max uJ vC)

Data identifying the first two projections and first map of a triangle-valued functor with named ordinary functors and a named natural transformation.

The endpoint isomorphisms point from the raw projections to the named functors. This orientation makes square the first component of the natural isomorphism from the raw family to its normalized form.

• obj₁Iso : T.comp π₁ ≅ F

  Identification of the raw first projection with the named source.

• obj₂Iso : T.comp π₂ ≅ G

  Identification of the raw second projection with the named target.

• square : CategoryStruct.comp (T.whiskerLeft π₁Toπ₂) self.obj₂Iso.hom = CategoryStruct.comp self.obj₁Iso.hom α

  The first map agrees with α after the endpoint identifications.

@[reducible, inline]

abbrev CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.third {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) : Functor J C

The unchanged third projected functor.

Equations

• N.third = T.comp CategoryTheory.Pretriangulated.Triangle.π₃

noncomputable def CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedSecond {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) : G ⟶ N.third

The second map transported from the named second vertex to the unchanged third vertex.

Equations

• N.normalizedSecond = CategoryTheory.CategoryStruct.comp N.obj₂Iso.inv (T.whiskerLeft CategoryTheory.Pretriangulated.Triangle.π₂Toπ₃)

noncomputable def CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedThird {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) : N.third ⟶ F.comp (CategoryTheory.shiftFunctor C 1)

The connecting map transported to the shift of the named first vertex.

Equations

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

noncomputable def CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedTriangle {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) : Functor J (Triangle C)

The normalized family, with literal first two vertices and literal first map.

Equations

• N.normalizedTriangle = CategoryTheory.Pretriangulated.Triangle.functorMk α N.normalizedSecond N.normalizedThird

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedTriangle_obj₁ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.normalizedTriangle.obj A).obj₁ = F.obj A

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedTriangle_obj₂ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.normalizedTriangle.obj A).obj₂ = G.obj A

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedTriangle_obj₃ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.normalizedTriangle.obj A).obj₃ = N.third.obj A

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedTriangle_mor₁ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.normalizedTriangle.obj A).mor₁ = α.app A

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedTriangle_mor₂ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.normalizedTriangle.obj A).mor₂ = N.normalizedSecond.app A

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedTriangle_mor₃ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.normalizedTriangle.obj A).mor₃ = N.normalizedThird.app A

noncomputable def CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.rawIsoNormalized {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) : T ≅ N.normalizedTriangle

The raw triangle family and its first-map-normalized form are naturally isomorphic. The comparison on the unchanged third projection is the identity.

Equations

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

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.rawIsoNormalized_hom_app_hom₁ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.rawIsoNormalized.hom.app A).hom₁ = N.obj₁Iso.hom.app A

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.rawIsoNormalized_hom_app_hom₂ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.rawIsoNormalized.hom.app A).hom₂ = N.obj₂Iso.hom.app A

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.rawIsoNormalized_hom_app_hom₃ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) (A : J) : (N.rawIsoNormalized.hom.app A).hom₃ = CategoryStruct.id (T.obj A).obj₃

Comparing two normalizations with the same first map

structure CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.ComparisonData {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T₁ T₂ : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N₁ : FirstMapNormalizationData T₁ F G α) (N₂ : FirstMapNormalizationData T₂ F G α) : Type (max uJ vC)

The remaining data needed for an endpoint-strict comparison of two first-map-normalized triangle families with the same named first two vertices and first map.

The interface fixes the first two comparison components to be identities. Thus only a natural isomorphism of the third vertices and compatibility with the second and third maps are stored.

• thirdIso : N₁.third ≅ N₂.third

  Natural comparison of the third vertices.

• second : CategoryStruct.comp N₁.normalizedSecond self.thirdIso.hom = N₂.normalizedSecond

  Compatibility with the maps from the common second vertex.

• third : N₁.normalizedThird = CategoryStruct.comp self.thirdIso.hom N₂.normalizedThird

  Compatibility with the connecting maps to the shifted common first vertex.

noncomputable def CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.ComparisonData.normalizedTriangleIso {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T₁ T₂ : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} {N₁ : FirstMapNormalizationData T₁ F G α} {N₂ : FirstMapNormalizationData T₂ F G α} (D : N₁.ComparisonData N₂) : N₁.normalizedTriangle ≅ N₂.normalizedTriangle

The natural isomorphism of normalized triangle families determined by the third-vertex comparison. Mathlib's triangle-functor constructor supplies the identity components on the common first two vertices.

Equations

• D.normalizedTriangleIso = CategoryTheory.Pretriangulated.Triangle.functorIsoMk' (CategoryTheory.Iso.refl F) (CategoryTheory.Iso.refl G) D.thirdIso ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.ComparisonData.normalizedTriangleIso_hom_app_hom₁ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T₁ T₂ : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} {N₁ : FirstMapNormalizationData T₁ F G α} {N₂ : FirstMapNormalizationData T₂ F G α} (D : N₁.ComparisonData N₂) (A : J) : (D.normalizedTriangleIso.hom.app A).hom₁ = CategoryStruct.id (N₁.normalizedTriangle.obj A).obj₁

The first component of the normalized comparison is the identity.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.ComparisonData.normalizedTriangleIso_hom_app_hom₂ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T₁ T₂ : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} {N₁ : FirstMapNormalizationData T₁ F G α} {N₂ : FirstMapNormalizationData T₂ F G α} (D : N₁.ComparisonData N₂) (A : J) : (D.normalizedTriangleIso.hom.app A).hom₂ = CategoryStruct.id (N₁.normalizedTriangle.obj A).obj₂

The second component of the normalized comparison is the identity.

@[simp]

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.ComparisonData.normalizedTriangleIso_hom_app_hom₃ {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T₁ T₂ : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} {N₁ : FirstMapNormalizationData T₁ F G α} {N₂ : FirstMapNormalizationData T₂ F G α} (D : N₁.ComparisonData N₂) (A : J) : (D.normalizedTriangleIso.hom.app A).hom₃ = D.thirdIso.hom.app A

The third component of the normalized comparison is the supplied natural isomorphism.

theorem CategoryTheory.Pretriangulated.Triangle.FirstMapNormalizationData.normalizedTriangle_obj_distinguished {J : Type uJ} {C : Type uC} [Category.{vJ, uJ} J] [Category.{vC, uC} C] [HasShift C ℤ] {T : Functor J (Triangle C)} {F G : Functor J C} {α : F ⟶ G} (N : FirstMapNormalizationData T F G α) [Limits.HasZeroObject C] [Preadditive C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [Pretriangulated C] (hT : ∀ (A : J), T.obj A ∈ distinguishedTriangles) (A : J) : N.normalizedTriangle.obj A ∈ distinguishedTriangles

Pointwise distinguishedness is preserved by first-map normalization.