From 58222ba4754ff4d6f308cc6163ef6c7e51daa7d9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 12 Jan 2026 14:52:53 +0100 Subject: [PATCH 1/3] feat(CategoryTheory/ComposableArrows): isIso_iff --- .../ComposableArrows/Basic.lean | 59 ++++++++++++------- .../CategoryTheory/ComposableArrows/Two.lean | 48 +++++++++++---- 2 files changed, 76 insertions(+), 31 deletions(-) diff --git a/Mathlib/CategoryTheory/ComposableArrows/Basic.lean b/Mathlib/CategoryTheory/ComposableArrows/Basic.lean index dfd780e1bfe77e..ccf6b34316a1c4 100644 --- a/Mathlib/CategoryTheory/ComposableArrows/Basic.lean +++ b/Mathlib/CategoryTheory/ComposableArrows/Basic.lean @@ -231,6 +231,11 @@ def isoMk₀ {F G : ComposableArrows C 0} (e : F.obj' 0 ≅ G.obj' 0) : F ≅ G hom := homMk₀ e.hom inv := homMk₀ e.inv +lemma isIso_iff₀ {F G : ComposableArrows C 0} (f : F ⟶ G) : + IsIso f ↔ IsIso (f.app 0) := by + rw [NatTrans.isIso_iff_isIso_app] + exact ⟨fun h ↦ h 0, fun _ i ↦ by fin_cases i; assumption⟩ + lemma ext₀ {F G : ComposableArrows C 0} (h : F.obj' 0 = G.obj 0) : F = G := ext (fun i => match i with | ⟨0, _⟩ => h) (fun i hi => by simp at hi) @@ -273,6 +278,11 @@ def isoMk₁ {F G : ComposableArrows C 1} lemma map'_eq_hom₁ (F : ComposableArrows C 1) : F.map' 0 1 = F.hom := rfl +lemma isIso_iff₁ {F G : ComposableArrows C 1} (f : F ⟶ G) : + IsIso f ↔ IsIso (f.app 0) ∧ IsIso (f.app 1) := by + rw [NatTrans.isIso_iff_isIso_app] + exact ⟨fun h ↦ ⟨h 0, h 1⟩, fun _ i ↦ by fin_cases i <;> tauto⟩ + lemma ext₁ {F G : ComposableArrows C 1} (left : F.left = G.left) (right : F.right = G.right) (w : F.hom = eqToHom left ≫ G.hom ≫ eqToHom right.symm) : F = G := @@ -398,23 +408,23 @@ def precomp {X : C} (f : X ⟶ F.left) : ComposableArrows C (n + 1) where map_comp g g' := Precomp.map_comp F f (leOfHom g) (leOfHom g') /-- Constructor for `ComposableArrows C 2`. -/ -@[simp] +@[reducible] def mk₂ {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) : ComposableArrows C 2 := (mk₁ g).precomp f /-- Constructor for `ComposableArrows C 3`. -/ -@[simp] +@[reducible] def mk₃ {X₀ X₁ X₂ X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : ComposableArrows C 3 := (mk₂ g h).precomp f /-- Constructor for `ComposableArrows C 4`. -/ -@[simp] +@[reducible] def mk₄ {X₀ X₁ X₂ X₃ X₄ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) : ComposableArrows C 4 := (mk₃ g h i).precomp f /-- Constructor for `ComposableArrows C 5`. -/ -@[simp] +@[reducible] def mk₅ {X₀ X₁ X₂ X₃ X₄ X₅ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) (j : X₄ ⟶ X₅) : ComposableArrows C 5 := @@ -512,7 +522,7 @@ def homMkSucc (α : F.obj' 0 ⟶ G.obj' 0) (β : F.δ₀ ⟶ G.δ₀) · exact naturality' β i (i + 1)) variable (α : F.obj' 0 ⟶ G.obj' 0) (β : F.δ₀ ⟶ G.δ₀) - (w : F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1) + (w : F.map' 0 1 ≫ app' β 0 = α ≫ G.map' 0 1 := by cat_disch) @[simp] lemma homMkSucc_app_zero : (homMkSucc α β w).app 0 = α := rfl @@ -575,8 +585,8 @@ section variable {f g : ComposableArrows C 2} (app₀ : f.obj' 0 ⟶ g.obj' 0) (app₁ : f.obj' 1 ⟶ g.obj' 1) (app₂ : f.obj' 2 ⟶ g.obj' 2) - (w₀ : f.map' 0 1 ≫ app₁ = app₀ ≫ g.map' 0 1) - (w₁ : f.map' 1 2 ≫ app₂ = app₁ ≫ g.map' 1 2) + (w₀ : f.map' 0 1 ≫ app₁ = app₀ ≫ g.map' 0 1 := by cat_disch) + (w₁ : f.map' 1 2 ≫ app₂ = app₁ ≫ g.map' 1 2 := by cat_disch) /-- Constructor for morphisms in `ComposableArrows C 2`. -/ def homMk₂ : f ⟶ g := homMkSucc app₀ (homMk₁ app₁ app₂ w₁) w₀ @@ -588,7 +598,10 @@ lemma homMk₂_app_zero : (homMk₂ app₀ app₁ app₂ w₀ w₁).app 0 = app lemma homMk₂_app_one : (homMk₂ app₀ app₁ app₂ w₀ w₁).app 1 = app₁ := rfl @[simp] -lemma homMk₂_app_two : (homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, by valid⟩ = app₂ := rfl +lemma homMk₂_app_two : (homMk₂ app₀ app₁ app₂ w₀ w₁).app 2 = app₂ := rfl + +@[simp] +lemma homMk₂_app_two' : (homMk₂ app₀ app₁ app₂ w₀ w₁).app ⟨2, by valid⟩ = app₂ := rfl end @@ -611,6 +624,11 @@ def isoMk₂ {f g : ComposableArrows C 2} (by rw [← cancel_epi app₁.hom, ← reassoc_of% w₁, app₂.hom_inv_id, comp_id, app₁.hom_inv_id_assoc]) +lemma isIso_iff₂ {F G : ComposableArrows C 2} (f : F ⟶ G) : + IsIso f ↔ IsIso (f.app 0) ∧ IsIso (f.app 1) ∧ IsIso (f.app 2) := by + rw [NatTrans.isIso_iff_isIso_app] + exact ⟨fun h ↦ ⟨h 0, h 1, h 2⟩, fun _ i ↦ by fin_cases i <;> tauto⟩ + lemma ext₂ {f g : ComposableArrows C 2} (h₀ : f.obj' 0 = g.obj' 0) (h₁ : f.obj' 1 = g.obj' 1) (h₂ : f.obj' 2 = g.obj' 2) (w₀ : f.map' 0 1 = eqToHom h₀ ≫ g.map' 0 1 ≫ eqToHom h₁.symm) @@ -639,9 +657,9 @@ variable {f g : ComposableArrows C 3} (app₀ : f.obj' 0 ⟶ g.obj' 0) (app₁ : f.obj' 1 ⟶ g.obj' 1) (app₂ : f.obj' 2 ⟶ g.obj' 2) (app₃ : f.obj' 3 ⟶ g.obj' 3) - (w₀ : f.map' 0 1 ≫ app₁ = app₀ ≫ g.map' 0 1) - (w₁ : f.map' 1 2 ≫ app₂ = app₁ ≫ g.map' 1 2) - (w₂ : f.map' 2 3 ≫ app₃ = app₂ ≫ g.map' 2 3) + (w₀ : f.map' 0 1 ≫ app₁ = app₀ ≫ g.map' 0 1 := by cat_disch) + (w₁ : f.map' 1 2 ≫ app₂ = app₁ ≫ g.map' 1 2 := by cat_disch) + (w₂ : f.map' 2 3 ≫ app₃ = app₂ ≫ g.map' 2 3 := by cat_disch) /-- Constructor for morphisms in `ComposableArrows C 3`. -/ def homMk₃ : f ⟶ g := homMkSucc app₀ (homMk₂ app₁ app₂ app₃ w₁ w₂) w₀ @@ -705,10 +723,10 @@ variable {f g : ComposableArrows C 4} (app₀ : f.obj' 0 ⟶ g.obj' 0) (app₁ : f.obj' 1 ⟶ g.obj' 1) (app₂ : f.obj' 2 ⟶ g.obj' 2) (app₃ : f.obj' 3 ⟶ g.obj' 3) (app₄ : f.obj' 4 ⟶ g.obj' 4) - (w₀ : f.map' 0 1 ≫ app₁ = app₀ ≫ g.map' 0 1) - (w₁ : f.map' 1 2 ≫ app₂ = app₁ ≫ g.map' 1 2) - (w₂ : f.map' 2 3 ≫ app₃ = app₂ ≫ g.map' 2 3) - (w₃ : f.map' 3 4 ≫ app₄ = app₃ ≫ g.map' 3 4) + (w₀ : f.map' 0 1 ≫ app₁ = app₀ ≫ g.map' 0 1 := by cat_disch) + (w₁ : f.map' 1 2 ≫ app₂ = app₁ ≫ g.map' 1 2 := by cat_disch) + (w₂ : f.map' 2 3 ≫ app₃ = app₂ ≫ g.map' 2 3 := by cat_disch) + (w₃ : f.map' 3 4 ≫ app₄ = app₃ ≫ g.map' 3 4 := by cat_disch) /-- Constructor for morphisms in `ComposableArrows C 4`. -/ def homMk₄ : f ⟶ g := homMkSucc app₀ (homMk₃ app₁ app₂ app₃ app₄ w₁ w₂ w₃) w₀ @@ -785,11 +803,11 @@ variable {f g : ComposableArrows C 5} (app₀ : f.obj' 0 ⟶ g.obj' 0) (app₁ : f.obj' 1 ⟶ g.obj' 1) (app₂ : f.obj' 2 ⟶ g.obj' 2) (app₃ : f.obj' 3 ⟶ g.obj' 3) (app₄ : f.obj' 4 ⟶ g.obj' 4) (app₅ : f.obj' 5 ⟶ g.obj' 5) - (w₀ : f.map' 0 1 ≫ app₁ = app₀ ≫ g.map' 0 1) - (w₁ : f.map' 1 2 ≫ app₂ = app₁ ≫ g.map' 1 2) - (w₂ : f.map' 2 3 ≫ app₃ = app₂ ≫ g.map' 2 3) - (w₃ : f.map' 3 4 ≫ app₄ = app₃ ≫ g.map' 3 4) - (w₄ : f.map' 4 5 ≫ app₅ = app₄ ≫ g.map' 4 5) + (w₀ : f.map' 0 1 ≫ app₁ = app₀ ≫ g.map' 0 1 := by cat_disch) + (w₁ : f.map' 1 2 ≫ app₂ = app₁ ≫ g.map' 1 2 := by cat_disch) + (w₂ : f.map' 2 3 ≫ app₃ = app₂ ≫ g.map' 2 3 := by cat_disch) + (w₃ : f.map' 3 4 ≫ app₄ = app₃ ≫ g.map' 3 4 := by cat_disch) + (w₄ : f.map' 4 5 ≫ app₅ = app₄ ≫ g.map' 4 5 := by cat_disch) /-- Constructor for morphisms in `ComposableArrows C 5`. -/ def homMk₅ : f ⟶ g := homMkSucc app₀ (homMk₄ app₁ app₂ app₃ app₄ app₅ w₁ w₂ w₃ w₄) w₀ @@ -943,7 +961,6 @@ def Functor.mapComposableArrowsObjMk₂Iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ (G.mapComposableArrows 2).obj (.mk₂ f g) ≅ .mk₂ (G.map f) (G.map g) := isoMk₂ (Iso.refl _) (Iso.refl _) (Iso.refl _) - suppress_compilation in /-- The functor `ComposableArrows C n ⥤ ComposableArrows D n` induced by `G : C ⥤ D` commutes with `opEquivalence`. -/ diff --git a/Mathlib/CategoryTheory/ComposableArrows/Two.lean b/Mathlib/CategoryTheory/ComposableArrows/Two.lean index c097dcc1688805..698a59be84e46d 100644 --- a/Mathlib/CategoryTheory/ComposableArrows/Two.lean +++ b/Mathlib/CategoryTheory/ComposableArrows/Two.lean @@ -22,20 +22,27 @@ and its faces (numbered from `0` to `2`) are respectively `mk₁ g`, @[expose] public section -universe v u - namespace CategoryTheory namespace ComposableArrows -variable {C : Type u} [Category.{v} C] - {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : f ≫ g = fg) +section + +variable {C : Type*} [Category* C] + {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) /-- The morphism `mk₁ f ⟶ mk₁ fg` when `f ≫ g = fg` for some morphism `g`. -/ -def twoδ₂Toδ₁ : +def twoδ₂Toδ₁ (h : f ≫ g = fg := by cat_disch) : mk₁ f ⟶ mk₁ fg := homMk₁ (𝟙 _) g +/-- The morphism `mk₁ fg ⟶ mk₁ g` when `f ≫ g = fg` for some morphism `f`. -/ +def twoδ₁Toδ₀ (h : f ≫ g = fg := by cat_disch) : + mk₁ fg ⟶ mk₁ g := + homMk₁ f (𝟙 _) + +variable (h : f ≫ g = fg) + @[simp] lemma twoδ₂Toδ₁_app_zero : (twoδ₂Toδ₁ f g fg h).app 0 = 𝟙 _ := rfl @@ -44,11 +51,6 @@ lemma twoδ₂Toδ₁_app_zero : lemma twoδ₂Toδ₁_app_one : (twoδ₂Toδ₁ f g fg h).app 1 = g := rfl -/-- The morphism `mk₁ fg ⟶ mk₁ g` when `f ≫ g = fg` for some morphism `f`. -/ -def twoδ₁Toδ₀ : - mk₁ fg ⟶ mk₁ g := - homMk₁ f (𝟙 _) - @[simp] lemma twoδ₁Toδ₀_app_zero : (twoδ₁Toδ₀ f g fg h).app 0 = f := rfl @@ -57,6 +59,32 @@ lemma twoδ₁Toδ₀_app_zero : lemma twoδ₁Toδ₀_app_one : (twoδ₁Toδ₀ f g fg h).app 1 = 𝟙 _ := rfl +instance [IsIso g] : IsIso (twoδ₂Toδ₁ f g fg h) := by + rw [isIso_iff₁] + constructor <;> dsimp <;> infer_instance + +instance [IsIso f] : IsIso (twoδ₁Toδ₀ f g fg h) := by + rw [isIso_iff₁] + constructor <;> dsimp <;> infer_instance + +end + +section + +variable {ι : Type*} [Preorder ι] (i₀ i₁ i₂ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) + +/-- Variant of `twoδ₁Toδ₀` for preorders. -/ +abbrev twoδ₁Toδ₀' : + mk₁ (homOfLE (hi₀₁.trans hi₁₂)) ⟶ mk₁ (homOfLE hi₁₂) := + twoδ₁Toδ₀ (homOfLE hi₀₁) _ _ rfl + +/-- Variant of `twoδ₂Toδ₁` for preorders. -/ +abbrev twoδ₂Toδ₁' : + mk₁ (homOfLE hi₀₁) ⟶ mk₁ (homOfLE (hi₀₁.trans hi₁₂)) := + twoδ₂Toδ₁ _ (homOfLE hi₁₂) _ rfl + +end + end ComposableArrows end CategoryTheory From c793021f5dbbebfe7a57df55cd4b1e387c4be4b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 12 Jan 2026 14:58:59 +0100 Subject: [PATCH 2/3] feat(CategoryTheory/ComposableArrows): compositions of three morphisms --- Mathlib.lean | 1 + .../ComposableArrows/Three.lean | 120 ++++++++++++++++++ 2 files changed, 121 insertions(+) create mode 100644 Mathlib/CategoryTheory/ComposableArrows/Three.lean diff --git a/Mathlib.lean b/Mathlib.lean index ebcfd3f8eca3b7..f7339b79acf875 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2380,6 +2380,7 @@ public import Mathlib.CategoryTheory.Comma.StructuredArrow.Functor public import Mathlib.CategoryTheory.Comma.StructuredArrow.Small public import Mathlib.CategoryTheory.ComposableArrows.Basic public import Mathlib.CategoryTheory.ComposableArrows.One +public import Mathlib.CategoryTheory.ComposableArrows.Three public import Mathlib.CategoryTheory.ComposableArrows.Two public import Mathlib.CategoryTheory.ConcreteCategory.Basic public import Mathlib.CategoryTheory.ConcreteCategory.Bundled diff --git a/Mathlib/CategoryTheory/ComposableArrows/Three.lean b/Mathlib/CategoryTheory/ComposableArrows/Three.lean new file mode 100644 index 00000000000000..c130d5051a1f24 --- /dev/null +++ b/Mathlib/CategoryTheory/ComposableArrows/Three.lean @@ -0,0 +1,120 @@ +/- +Copyright (c) 2025 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +module + +public import Mathlib.CategoryTheory.ComposableArrows.Basic + +/-! +# API for compositions of three arrows + +Given morphisms `f₁ : i ⟶ j`, `f₂ : j ⟶ k`, `f₃ : k ⟶ l`, and their +compositions `f₁₂ : i ⟶ k` and `f₂₃ : j ⟶ l`, we define +maps `ComposableArrows.threeδ₃Toδ₂ : mk₂ f₁ f₂ ⟶ mk₂ f₁ f₂₃`, +`threeδ₂Toδ₁ : mk₂ f₁ f₂₃ ⟶ mk₂ f₁₂ f₃`, and `threeδ₁Toδ₀ : mk₂ f₁₂ f₃ ⟶ mk₂ f₂ f₃`. +The names are justified by the fact that `ComposableArrow.mk₃ f₁ f₂ f₃` +can be thought of as a `3`-simplex in the simplicial set `nerve C`, +and its faces (numbered from `0` to `3`) are respectively +`mk₂ f₂ f₃`, `mk₂ f₁₂ f₃`, `mk₂ f₁ f₂₃`, `mk₂ f₁ f₂`. + +-/ + +@[expose] public section + +universe v u + +namespace CategoryTheory + +namespace ComposableArrows + +section + +variable {C : Type u} [Category.{v} C] + {i j k l : C} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) + (f₁₂ : i ⟶ k) (f₂₃ : j ⟶ l) + +/-- The morphism `mk₂ f₁ f₂ ⟶ mk₂ f₁ f₂₃` when `f₂ ≫ f₃ = f₂₃`. -/ +def threeδ₃Toδ₂ (h₂₃ : f₂ ≫ f₃ = f₂₃ := by cat_disch) : + mk₂ f₁ f₂ ⟶ mk₂ f₁ f₂₃ := + homMk₂ (𝟙 _) (𝟙 _) f₃ + +/-- The morphism `mk₂ f₁ f₂₃ ⟶ mk₂ f₁₂ f₃` when `f₁ ≫ f₂ = f₁₂` and `f₂ ≫ f₃ = f₂₃`. -/ +def threeδ₂Toδ₁ (h₁₂ : f₁ ≫ f₂ = f₁₂ := by cat_disch) (h₂₃ : f₂ ≫ f₃ = f₂₃ := by cat_disch) : + mk₂ f₁ f₂₃ ⟶ mk₂ f₁₂ f₃ := + homMk₂ (𝟙 _) f₂ (𝟙 _) + +/-- The morphism `mk₂ f₁₂ f₃ ⟶ mk₂ f₂ f₃` when `f₁ ≫ f₂ = f₁₂`. -/ +def threeδ₁Toδ₀ (h₁₂ : f₁ ≫ f₂ = f₁₂ := by cat_disch) : + mk₂ f₁₂ f₃ ⟶ mk₂ f₂ f₃ := + homMk₂ f₁ (𝟙 _) (𝟙 _) + +variable (h₁₂ : f₁ ≫ f₂ = f₁₂) (h₂₃ : f₂ ≫ f₃ = f₂₃) + +@[simp] +lemma threeδ₃Toδ₂_app_zero : + (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 0 = 𝟙 _ := rfl + +@[simp] +lemma threeδ₃Toδ₂_app_one : + (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 1 = 𝟙 _ := rfl + +@[simp] +lemma threeδ₃Toδ₂_app_two : + (threeδ₃Toδ₂ f₁ f₂ f₃ f₂₃ h₂₃).app 2 = f₃ := rfl + +@[simp] +lemma threeδ₂Toδ₁_app_zero : + (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 0 = 𝟙 _ := rfl + +@[simp] +lemma threeδ₂Toδ₁_app_one : + (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 1 = f₂ := rfl + +@[simp] +lemma threeδ₂Toδ₁_app_two : + (threeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃).app 2 = 𝟙 _ := rfl + +@[simp] +lemma threeδ₁Toδ₀_app_zero : + (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 0 = f₁ := rfl + +@[simp] +lemma threeδ₁Toδ₀_app_one : + (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 1 = (𝟙 _) := rfl + +@[simp] +lemma threeδ₁Toδ₀_app_two : + (threeδ₁Toδ₀ f₁ f₂ f₃ f₁₂ h₁₂).app 2 = (𝟙 _) := rfl + +end + +section + +variable {ι : Type*} [Preorder ι] + (i₀ i₁ i₂ i₃ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) + +/-- Variant of `threeδ₃Toδ₂` for preorders. -/ +abbrev threeδ₃Toδ₂' : + mk₂ (homOfLE hi₀₁) (homOfLE hi₁₂) ⟶ + mk₂ (homOfLE hi₀₁) (homOfLE (hi₁₂.trans hi₂₃)) := + threeδ₃Toδ₂ _ _ (homOfLE hi₂₃) _ rfl + +/-- Variant of `threeδ₂Toδ₁` for preorders. -/ +abbrev threeδ₂Toδ₁' : + mk₂ (homOfLE hi₀₁) (homOfLE (hi₁₂.trans hi₂₃)) ⟶ + mk₂ (homOfLE (hi₀₁.trans hi₁₂)) (homOfLE hi₂₃) := + threeδ₂Toδ₁ _ (homOfLE hi₁₂) _ _ _ rfl rfl + +/-- Variant of `threeδ₁Toδ₀` for preorders. -/ +abbrev threeδ₁Toδ₀' : + mk₂ (homOfLE (hi₀₁.trans hi₁₂)) (homOfLE hi₂₃) ⟶ + mk₂ (homOfLE hi₁₂) (homOfLE hi₂₃) := + threeδ₁Toδ₀ (homOfLE hi₀₁) _ _ _ rfl + +end + +end ComposableArrows + +end CategoryTheory From f24266f56e3197197a34d8a10c899da475115113 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Fri, 16 Jan 2026 18:05:51 +0100 Subject: [PATCH 3/3] s/reducible/abbrev/ --- Mathlib/CategoryTheory/ComposableArrows/Basic.lean | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/Mathlib/CategoryTheory/ComposableArrows/Basic.lean b/Mathlib/CategoryTheory/ComposableArrows/Basic.lean index ccf6b34316a1c4..899b64fdd78739 100644 --- a/Mathlib/CategoryTheory/ComposableArrows/Basic.lean +++ b/Mathlib/CategoryTheory/ComposableArrows/Basic.lean @@ -408,24 +408,20 @@ def precomp {X : C} (f : X ⟶ F.left) : ComposableArrows C (n + 1) where map_comp g g' := Precomp.map_comp F f (leOfHom g) (leOfHom g') /-- Constructor for `ComposableArrows C 2`. -/ -@[reducible] -def mk₂ {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) : ComposableArrows C 2 := +abbrev mk₂ {X₀ X₁ X₂ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) : ComposableArrows C 2 := (mk₁ g).precomp f /-- Constructor for `ComposableArrows C 3`. -/ -@[reducible] -def mk₃ {X₀ X₁ X₂ X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : ComposableArrows C 3 := +abbrev mk₃ {X₀ X₁ X₂ X₃ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) : ComposableArrows C 3 := (mk₂ g h).precomp f /-- Constructor for `ComposableArrows C 4`. -/ -@[reducible] -def mk₄ {X₀ X₁ X₂ X₃ X₄ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) : +abbrev mk₄ {X₀ X₁ X₂ X₃ X₄ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) : ComposableArrows C 4 := (mk₃ g h i).precomp f /-- Constructor for `ComposableArrows C 5`. -/ -@[reducible] -def mk₅ {X₀ X₁ X₂ X₃ X₄ X₅ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) +abbrev mk₅ {X₀ X₁ X₂ X₃ X₄ X₅ : C} (f : X₀ ⟶ X₁) (g : X₁ ⟶ X₂) (h : X₂ ⟶ X₃) (i : X₃ ⟶ X₄) (j : X₄ ⟶ X₅) : ComposableArrows C 5 := (mk₄ g h i j).precomp f