From 3e6da1b57dce9b51bf8010e0281674201f6814cc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 16 Feb 2026 09:54:45 +0100 Subject: [PATCH 01/13] chosen pullbacks --- Mathlib.lean | 1 + .../Shapes/Pullback/ChosenPullback.lean | 255 ++++++++++++++++++ .../Shapes/Pullback/IsPullback/Basic.lean | 18 ++ 3 files changed, 274 insertions(+) create mode 100644 Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean diff --git a/Mathlib.lean b/Mathlib.lean index cd72d6d36a5d31..07220fa37455a5 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2752,6 +2752,7 @@ public import Mathlib.CategoryTheory.Limits.Shapes.Products public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform +public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Connected public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean new file mode 100644 index 00000000000000..d3309055f83185 --- /dev/null +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -0,0 +1,255 @@ +/- +Copyright (c) 2026 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou, Christian Merten +-/ +module + +public import Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic + +/-! +# Chosen pullbacks + +Given two morphisms `f₁ : X₁ ⟶ S` and `f₂ : X₂ ⟶ S`, we introduce +a structure `ChosenPullback f₁ f₂` which contains the data of +pullback of `f₁` and `f₂`. + +## TODO +* relate this to `ChosenPullbacksAlong` which is defined in +`LocallyCartesianClosed.ChosenPullbacksAlong`. + +-/ + +@[expose] public section + +universe v u + +namespace CategoryTheory.Limits + +variable {C : Type u} [Category.{v} C] + +/-- Given two morphisms `f₁ : X₁ ⟶ S` and `f₂ : X₂ ⟶ S`, this is the choice +of a pullback of `f₁` and `f₂`. -/ +structure ChosenPullback {X₁ X₂ S : C} (f₁ : X₁ ⟶ S) (f₂ : X₂ ⟶ S) where + /-- the pullback -/ + pullback : C + /-- the first projection -/ + p₁ : pullback ⟶ X₁ + /-- the second projection -/ + p₂ : pullback ⟶ X₂ + condition : p₁ ≫ f₁ = p₂ ≫ f₂ + /-- `pullback` is a pullback of `f₁` and `f₂` -/ + isLimit : IsLimit (PullbackCone.mk _ _ condition) + /-- the projection `pullback ⟶ S` -/ + p : pullback ⟶ S := p₁ ≫ f₁ + hp₁ : p₁ ≫ f₁ = p := by cat_disch + +namespace ChosenPullback + +section + +variable {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} + (h : ChosenPullback f₁ f₂) + +attribute [reassoc] condition + +lemma isPullback : IsPullback h.p₁ h.p₂ f₁ f₂ where + w := h.condition + isLimit' := ⟨h.isLimit⟩ + +attribute [reassoc (attr := simp)] hp₁ + +@[reassoc (attr := simp)] +lemma hp₂ : h.p₂ ≫ f₂ = h.p := by rw [← h.condition, hp₁] + +/-- Given `f₁ : X₁ ⟶ S`, `f₂ : X₂ ⟶ S`, `h : ChosenPullback f₁ f₂` and morphisms +`g₁ : Y ⟶ X₁`, `g₂ : Y ⟶ X₂` and `b : Y ⟶ S`, this structure contains a morphism +`Y ⟶ h.pullback` such that `f ≫ h.p₁ = g₁`, `f ≫ h.p₂ = g₂` and `f ≫ h.p = b`. +(This is nonempty only when `g₁ ≫ f₁ = g₂ ≫ f₂ = b`.) -/ +structure LiftStruct {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (b : Y ⟶ S) where + /-- a lifting to the pullback -/ + f : Y ⟶ h.pullback + f_p₁ : f ≫ h.p₁ = g₁ + f_p₂ : f ≫ h.p₂ = g₂ + f_p : f ≫ h.p = b + +namespace LiftStruct + +attribute [reassoc (attr := simp)] f_p₁ f_p₂ f_p + +variable {h} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (l : h.LiftStruct g₁ g₂ b) + +include l in +@[reassoc] +lemma w : g₁ ≫ f₁ = g₂ ≫ f₂ := by + simp only [← l.f_p₁, ← l.f_p₂, Category.assoc, h.condition] + +instance : Subsingleton (h.LiftStruct g₁ g₂ b) where + allEq := by + rintro ⟨f, f_p₁, f_p₂, _⟩ ⟨f', f'_p₁, f'_p₂, _⟩ + obtain rfl : f = f' := by + apply h.isPullback.hom_ext + · rw [f_p₁, f'_p₁] + · rw [f_p₂, f'_p₂] + rfl + +lemma nonempty (w : g₁ ≫ f₁ = g₂ ≫ f₂) (hf₁ : g₁ ≫ f₁ = b) : + Nonempty (h.LiftStruct g₁ g₂ b) := by + obtain ⟨l, h₁, h₂⟩ := h.isPullback.exists_lift g₁ g₂ w + exact ⟨{ + f := l + f_p₁ := h₁ + f_p₂ := h₂ + f_p := by rw [← h.hp₁, ← hf₁, reassoc_of% h₁] + }⟩ + +end LiftStruct + +end + +variable {X S : C} {f : X ⟶ S} (h : ChosenPullback f f) + +/-- Given `f : X ⟶ S` and `h : ChosenPullback f f`, this is the type of +morphisms `l : X ⟶ h.pullback` that are equal to the diagonal map. -/ +abbrev Diagonal := h.LiftStruct (𝟙 X) (𝟙 X) f + +instance : Nonempty h.Diagonal := by apply LiftStruct.nonempty <;> cat_disch + +end ChosenPullback + +variable {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S} + (h₁₂ : ChosenPullback f₁ f₂) (h₂₃ : ChosenPullback f₂ f₃) (h₁₃ : ChosenPullback f₁ f₃) + +/-- Given three morphisms `f₁ : X₁ ⟶ S`, `f₂ : X₂ ⟶ S` and `f₃ : X₃ ⟶ S`, and chosen +pullbacks for `(f₁, f₂)`, `(f₂, f₃)` and `(f₁, f₃)`, this structure contains the data +of a wide pullback of the three morphisms `f₁`, `f₂` and `f₃`. -/ +structure ChosenPullback₃ where + /-- A chosen pullback of `h₁₂.pullback` and `h₂₃.pullback` over `X₂`. -/ + chosenPullback : ChosenPullback h₁₂.p₂ h₂₃.p₁ + /-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `S`. -/ + p : chosenPullback.pullback ⟶ S := chosenPullback.p₁ ≫ h₁₂.p + /-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₁`. -/ + p₁ : chosenPullback.pullback ⟶ X₁ := chosenPullback.p₁ ≫ h₁₂.p₁ + /-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₃`. -/ + p₃ : chosenPullback.pullback ⟶ X₃ := chosenPullback.p₂ ≫ h₂₃.p₂ + /-- A morphism from the wide pullback `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₃` + that is compatible with projections. -/ + l : h₁₃.LiftStruct p₁ p₃ p + hp₁ : chosenPullback.p₁ ≫ h₁₂.p₁ = p₁ := by cat_disch + hp₃ : chosenPullback.p₂ ≫ h₂₃.p₂ = p₃ := by cat_disch + +namespace ChosenPullback₃ + +variable {h₁₂ h₂₃ h₁₃} (h : ChosenPullback₃ h₁₂ h₂₃ h₁₃) + +/-- The chosen wide pullback of `(f₁, f₂, f₃)`. -/ +abbrev pullback := h.chosenPullback.pullback + +/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₃`. -/ +def p₁₃ : h.pullback ⟶ h₁₃.pullback := h.l.f + +/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₁` and `f₂`. -/ +def p₁₂ : h.pullback ⟶ h₁₂.pullback := h.chosenPullback.p₁ + +/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to the pullback of `f₂` and `f₃`. -/ +def p₂₃ : h.pullback ⟶ h₂₃.pullback := h.chosenPullback.p₂ + +/-- The projection from the wide pullback of `(f₁, f₂, f₃)` to `X₂`. -/ +def p₂ : h.pullback ⟶ X₂ := h.chosenPullback.p + +@[reassoc (attr := simp)] +lemma p₁₂_p₁ : h.p₁₂ ≫ h₁₂.p₁ = h.p₁ := by simp [p₁₂, hp₁] + +@[reassoc (attr := simp)] +lemma p₁₂_p₂ : h.p₁₂ ≫ h₁₂.p₂ = h.p₂ := by simp [p₁₂, p₂] + +@[reassoc (attr := simp)] +lemma p₂₃_p₂ : h.p₂₃ ≫ h₂₃.p₁ = h.p₂ := by simp [p₂₃, p₂] + +@[reassoc (attr := simp)] +lemma p₂₃_p₃ : h.p₂₃ ≫ h₂₃.p₂ = h.p₃ := by simp [p₂₃, hp₃] + +@[reassoc (attr := simp)] +lemma p₁₃_p₁ : h.p₁₃ ≫ h₁₃.p₁ = h.p₁ := by simp [p₁₃] + +@[reassoc (attr := simp)] +lemma p₁₃_p₃ : h.p₁₃ ≫ h₁₃.p₂ = h.p₃ := by simp [p₁₃] + +@[reassoc (attr := simp)] +lemma w₁ : h.p₁ ≫ f₁ = h.p := by + simpa only [← hp₁, Category.assoc, h₁₃.hp₁, h.l.f_p] using h.l.f_p₁.symm =≫ f₁ + +@[reassoc (attr := simp)] +lemma w₃ : h.p₃ ≫ f₃ = h.p := by + simpa only [← hp₃, Category.assoc, h₁₃.hp₂, h.l.f_p] using h.l.f_p₂.symm =≫ f₃ + +@[reassoc (attr := simp)] +lemma w₂ : h.p₂ ≫ f₂ = h.p := by + rw [← p₂₃_p₂_assoc, h₂₃.condition, ← w₃, p₂₃_p₃_assoc] + +@[reassoc (attr := simp)] +lemma p₁₂_p : h.p₁₂ ≫ h₁₂.p = h.p := by + rw [← h₁₂.hp₂, p₁₂_p₂_assoc, w₂] + +@[reassoc (attr := simp)] +lemma p₂₃_p : h.p₂₃ ≫ h₂₃.p = h.p := by + rw [← h₂₃.hp₂, p₂₃_p₃_assoc, w₃] + +@[reassoc (attr := simp)] +lemma p₁₃_p : h.p₁₃ ≫ h₁₃.p = h.p := by + rw [← h₁₃.hp₁, p₁₃_p₁_assoc, w₁] + +lemma p₁₂_eq_lift : h.p₁₂ = h₁₂.isPullback.lift h.p₁ h.p₂ (by simp) := by + apply h₁₂.isPullback.hom_ext <;> simp + +lemma p₂₃_eq_lift : h.p₂₃ = h₂₃.isPullback.lift h.p₂ h.p₃ (by simp) := by + apply h₂₃.isPullback.hom_ext <;> simp + +lemma p₁₃_eq_lift : h.p₁₃ = h₁₃.isPullback.lift h.p₁ h.p₃ (by simp) := by + apply h₁₃.isPullback.hom_ext <;> simp + +lemma exists_lift {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (g₃ : Y ⟶ X₃) (b : Y ⟶ S) + (hg₁ : g₁ ≫ f₁ = b) (hg₂ : g₂ ≫ f₂ = b) (hg₃ : g₃ ≫ f₃ = b) : + ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃ := by + obtain ⟨φ₁₂, w₁, w₂⟩ := h₁₂.isPullback.exists_lift g₁ g₂ (by aesop) + obtain ⟨φ₂₃, w₂', w₃⟩ := h₂₃.isPullback.exists_lift g₂ g₃ (by aesop) + obtain ⟨φ, w₁₂, w₂₃⟩ := h.chosenPullback.isPullback.exists_lift φ₁₂ φ₂₃ (by aesop) + refine ⟨φ, ?_, ?_, ?_⟩ + · rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁] + · rw [← w₂, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₂] + · rw [← w₃, ← w₂₃, Category.assoc, ← p₂₃, p₂₃_p₃] + +lemma isPullback₂ : IsPullback h.p₁₂ h.p₂₃ h₁₂.p₂ h₂₃.p₁ := h.chosenPullback.isPullback + +lemma hom_ext {Y : C} {φ φ' : Y ⟶ h.pullback} + (h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁) (h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂) + (h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃) : φ = φ' := by + apply h.isPullback₂.hom_ext + · apply h₁₂.isPullback.hom_ext <;> simpa + · apply h₂₃.isPullback.hom_ext <;> simpa + +lemma isPullback₁ : IsPullback h.p₁₂ h.p₁₃ h₁₂.p₁ h₁₃.p₁ := + .mk' (by simp) (fun _ _ _ h₁ h₂ ↦ h.hom_ext (by simpa using h₁ =≫ h₁₂.p₁) + (by simpa using h₁ =≫ h₁₂.p₂) (by simpa using h₂ =≫ h₁₃.p₂)) + (fun _ a b w ↦ by + obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ := + h.exists_lift (a ≫ h₁₂.p₁) (a ≫ h₁₂.p₂) (b ≫ h₁₃.p₂) _ rfl + (by simp) (by simpa using w.symm =≫ f₁) + refine ⟨φ, ?_, ?_⟩ + · apply h₁₂.isPullback.hom_ext <;> simpa + · apply h₁₃.isPullback.hom_ext <;> aesop) + +lemma isPullback₃ : IsPullback h.p₁₃ h.p₂₃ h₁₃.p₂ h₂₃.p₂ := + .mk' (by simp) (fun _ _ _ h₁ h₂ ↦ h.hom_ext (by simpa using h₁ =≫ h₁₃.p₁) + (by simpa using h₂ =≫ h₂₃.p₁) (by simpa using h₁ =≫ h₁₃.p₂)) + (fun _ a b w ↦ by + obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ := + h.exists_lift (a ≫ h₁₃.p₁) (b ≫ h₂₃.p₁) (a ≫ h₁₃.p₂) _ rfl + (by simpa using w.symm =≫ f₃) (by simp) + refine ⟨φ, ?_, ?_⟩ + · apply h₁₃.isPullback.hom_ext <;> simpa + · apply h₂₃.isPullback.hom_ext <;> cat_disch) + +end ChosenPullback₃ + +end CategoryTheory.Limits diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean index d31bfc36f73ccc..8a0bf56663ecc2 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean @@ -356,6 +356,24 @@ lemma of_isLimit_binaryFan_of_isTerminal rfl)⟩ end +lemma mk' {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} + (w : fst ≫ f = snd ≫ g) + (hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : T ⟶ P⦄ (_ : φ ≫ fst = φ' ≫ fst) + (_ : φ ≫ snd = φ' ≫ snd), φ = φ') + (exists_lift : ∀ ⦃T : C⦄ (a : T ⟶ X) (b : T ⟶ Y) + (_ : a ≫ f = b ≫ g), ∃ (l : T ⟶ P), l ≫ fst = a ∧ l ≫ snd = b) : + IsPullback fst snd f g where + w := w + isLimit' := by + let l (s : PullbackCone f g) := exists_lift _ _ s.condition + exact ⟨PullbackCone.IsLimit.mk _ + (fun s ↦ (l s).choose) + (fun s ↦ (l s).choose_spec.1) + (fun s ↦ (l s).choose_spec.2) + (fun s m h₁ h₂ ↦ hom_ext + (h₁.trans (l s).choose_spec.1.symm) + (h₂.trans (l s).choose_spec.2.symm))⟩ + end IsPullback namespace IsPushout From 2ff2762b8e4b26e488c35fe4dcb40de48dee056d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 16 Feb 2026 09:57:17 +0100 Subject: [PATCH 02/13] cat_disch --- .../Limits/Shapes/Pullback/ChosenPullback.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index d3309055f83185..d5321aa9547e29 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -211,9 +211,9 @@ lemma p₁₃_eq_lift : h.p₁₃ = h₁₃.isPullback.lift h.p₁ h.p₃ (by si lemma exists_lift {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (g₃ : Y ⟶ X₃) (b : Y ⟶ S) (hg₁ : g₁ ≫ f₁ = b) (hg₂ : g₂ ≫ f₂ = b) (hg₃ : g₃ ≫ f₃ = b) : ∃ (φ : Y ⟶ h.pullback), φ ≫ h.p₁ = g₁ ∧ φ ≫ h.p₂ = g₂ ∧ φ ≫ h.p₃ = g₃ := by - obtain ⟨φ₁₂, w₁, w₂⟩ := h₁₂.isPullback.exists_lift g₁ g₂ (by aesop) - obtain ⟨φ₂₃, w₂', w₃⟩ := h₂₃.isPullback.exists_lift g₂ g₃ (by aesop) - obtain ⟨φ, w₁₂, w₂₃⟩ := h.chosenPullback.isPullback.exists_lift φ₁₂ φ₂₃ (by aesop) + obtain ⟨φ₁₂, w₁, w₂⟩ := h₁₂.isPullback.exists_lift g₁ g₂ (by cat_disch) + obtain ⟨φ₂₃, w₂', w₃⟩ := h₂₃.isPullback.exists_lift g₂ g₃ (by cat_disch) + obtain ⟨φ, w₁₂, w₂₃⟩ := h.chosenPullback.isPullback.exists_lift φ₁₂ φ₂₃ (by cat_disch) refine ⟨φ, ?_, ?_, ?_⟩ · rw [← w₁, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₁] · rw [← w₂, ← w₁₂, Category.assoc, ← p₁₂, p₁₂_p₂] @@ -237,7 +237,7 @@ lemma isPullback₁ : IsPullback h.p₁₂ h.p₁₃ h₁₂.p₁ h₁₃.p₁ : (by simp) (by simpa using w.symm =≫ f₁) refine ⟨φ, ?_, ?_⟩ · apply h₁₂.isPullback.hom_ext <;> simpa - · apply h₁₃.isPullback.hom_ext <;> aesop) + · apply h₁₃.isPullback.hom_ext <;> cat_disch) lemma isPullback₃ : IsPullback h.p₁₃ h.p₂₃ h₁₃.p₂ h₂₃.p₂ := .mk' (by simp) (fun _ _ _ h₁ h₂ ↦ h.hom_ext (by simpa using h₁ =≫ h₁₃.p₁) From 0e70131d47934e890038a943f0b0eb1d6c00f2bf Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 17 Feb 2026 19:35:23 +0100 Subject: [PATCH 03/13] Update Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../Limits/Shapes/Pullback/ChosenPullback.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index d5321aa9547e29..d21e5c999c84fa 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -69,9 +69,9 @@ lemma hp₂ : h.p₂ ≫ f₂ = h.p := by rw [← h.condition, hp₁] structure LiftStruct {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (b : Y ⟶ S) where /-- a lifting to the pullback -/ f : Y ⟶ h.pullback - f_p₁ : f ≫ h.p₁ = g₁ - f_p₂ : f ≫ h.p₂ = g₂ - f_p : f ≫ h.p = b + f_p₁ : f ≫ h.p₁ = g₁ := by cat_disch + f_p₂ : f ≫ h.p₂ = g₂ := by cat_disch + f_p : f ≫ h.p = b := by cat_disch namespace LiftStruct From 29fa64a43cfbf6ec86a84657a806b567cddb8001 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 17 Feb 2026 19:35:42 +0100 Subject: [PATCH 04/13] Update Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index d21e5c999c84fa..9fd66b3d6e79a4 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -100,8 +100,7 @@ lemma nonempty (w : g₁ ≫ f₁ = g₂ ≫ f₂) (hf₁ : g₁ ≫ f₁ = b) : f := l f_p₁ := h₁ f_p₂ := h₂ - f_p := by rw [← h.hp₁, ← hf₁, reassoc_of% h₁] - }⟩ + f_p := by rw [← h.hp₁, ← hf₁, reassoc_of% h₁] }⟩ end LiftStruct From f728e8f847a6fb9d906efd1def9be35d2012416d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 17 Feb 2026 19:35:54 +0100 Subject: [PATCH 05/13] Update Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../Limits/Shapes/Pullback/ChosenPullback.lean | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index 9fd66b3d6e79a4..e310062968ec2c 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -87,10 +87,7 @@ lemma w : g₁ ≫ f₁ = g₂ ≫ f₂ := by instance : Subsingleton (h.LiftStruct g₁ g₂ b) where allEq := by rintro ⟨f, f_p₁, f_p₂, _⟩ ⟨f', f'_p₁, f'_p₂, _⟩ - obtain rfl : f = f' := by - apply h.isPullback.hom_ext - · rw [f_p₁, f'_p₁] - · rw [f_p₂, f'_p₂] + obtain rfl : f = f' := by apply h.isPullback.hom_ext <;> grind rfl lemma nonempty (w : g₁ ≫ f₁ = g₂ ≫ f₂) (hf₁ : g₁ ≫ f₁ = b) : From dacb767d9c1aca08c5e2d8a0efb79346faf6d8be Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 17 Feb 2026 19:36:11 +0100 Subject: [PATCH 06/13] Update Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index e310062968ec2c..31ebebfde0a142 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -217,6 +217,7 @@ lemma exists_lift {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (g₃ : Y ⟶ lemma isPullback₂ : IsPullback h.p₁₂ h.p₂₃ h₁₂.p₂ h₂₃.p₁ := h.chosenPullback.isPullback +@[ext] lemma hom_ext {Y : C} {φ φ' : Y ⟶ h.pullback} (h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁) (h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂) (h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃) : φ = φ' := by From 82fbe7875224493c0a8a83a54285756fc6f69a7b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 17 Feb 2026 19:36:27 +0100 Subject: [PATCH 07/13] Update Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index 31ebebfde0a142..d16babdce192f8 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -75,7 +75,7 @@ structure LiftStruct {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (b : Y ⟶ namespace LiftStruct -attribute [reassoc (attr := simp)] f_p₁ f_p₂ f_p +attribute [reassoc (attr := simp, grind =)] f_p₁ f_p₂ f_p variable {h} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (l : h.LiftStruct g₁ g₂ b) From 80725de0e1f4bc893fd5c8a3ea821b8386d6e3e9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 17 Feb 2026 19:36:44 +0100 Subject: [PATCH 08/13] Update Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index d16babdce192f8..81b901da7aabe7 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -59,7 +59,7 @@ lemma isPullback : IsPullback h.p₁ h.p₂ f₁ f₂ where attribute [reassoc (attr := simp)] hp₁ -@[reassoc (attr := simp)] +@[reassoc (attr := simp, grind =)] lemma hp₂ : h.p₂ ≫ f₂ = h.p := by rw [← h.condition, hp₁] /-- Given `f₁ : X₁ ⟶ S`, `f₂ : X₂ ⟶ S`, `h : ChosenPullback f₁ f₂` and morphisms From aab3c225029ccc13fcedcd95e9060cb9bd135cf2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= <37772949+joelriou@users.noreply.github.com> Date: Tue, 17 Feb 2026 19:37:03 +0100 Subject: [PATCH 09/13] Update Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com> --- .../CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index 81b901da7aabe7..b8b87d86b71213 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -57,7 +57,7 @@ lemma isPullback : IsPullback h.p₁ h.p₂ f₁ f₂ where w := h.condition isLimit' := ⟨h.isLimit⟩ -attribute [reassoc (attr := simp)] hp₁ +attribute [reassoc (attr := simp, grind =)] hp₁ @[reassoc (attr := simp, grind =)] lemma hp₂ : h.p₂ ≫ f₂ = h.p := by rw [← h.condition, hp₁] From 2723f694eed8f7fc08c7a8392645bc31f0de5999 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 17 Feb 2026 19:45:16 +0100 Subject: [PATCH 10/13] cleaning up --- .../Shapes/Pullback/ChosenPullback.lean | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index b8b87d86b71213..a8f07a05d4f6a6 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -62,6 +62,12 @@ attribute [reassoc (attr := simp, grind =)] hp₁ @[reassoc (attr := simp, grind =)] lemma hp₂ : h.p₂ ≫ f₂ = h.p := by rw [← h.condition, hp₁] +@[ext] +lemma hom_ext {Y : C} {f g : Y ⟶ h.pullback} + (h₁ : f ≫ h.p₁ = g ≫ h.p₁) (h₂ : f ≫ h.p₂ = g ≫ h.p₂) : + f = g := + h.isPullback.hom_ext h₁ h₂ + /-- Given `f₁ : X₁ ⟶ S`, `f₂ : X₂ ⟶ S`, `h : ChosenPullback f₁ f₂` and morphisms `g₁ : Y ⟶ X₁`, `g₂ : Y ⟶ X₂` and `b : Y ⟶ S`, this structure contains a morphism `Y ⟶ h.pullback` such that `f ≫ h.p₁ = g₁`, `f ≫ h.p₂ = g₂` and `f ≫ h.p = b`. @@ -87,7 +93,7 @@ lemma w : g₁ ≫ f₁ = g₂ ≫ f₂ := by instance : Subsingleton (h.LiftStruct g₁ g₂ b) where allEq := by rintro ⟨f, f_p₁, f_p₂, _⟩ ⟨f', f'_p₁, f'_p₂, _⟩ - obtain rfl : f = f' := by apply h.isPullback.hom_ext <;> grind + obtain rfl : f = f' := by cat_disch rfl lemma nonempty (w : g₁ ≫ f₁ = g₂ ≫ f₂) (hf₁ : g₁ ≫ f₁ = b) : @@ -196,13 +202,13 @@ lemma p₁₃_p : h.p₁₃ ≫ h₁₃.p = h.p := by rw [← h₁₃.hp₁, p₁₃_p₁_assoc, w₁] lemma p₁₂_eq_lift : h.p₁₂ = h₁₂.isPullback.lift h.p₁ h.p₂ (by simp) := by - apply h₁₂.isPullback.hom_ext <;> simp + cat_disch lemma p₂₃_eq_lift : h.p₂₃ = h₂₃.isPullback.lift h.p₂ h.p₃ (by simp) := by - apply h₂₃.isPullback.hom_ext <;> simp + cat_disch lemma p₁₃_eq_lift : h.p₁₃ = h₁₃.isPullback.lift h.p₁ h.p₃ (by simp) := by - apply h₁₃.isPullback.hom_ext <;> simp + cat_disch lemma exists_lift {Y : C} (g₁ : Y ⟶ X₁) (g₂ : Y ⟶ X₂) (g₃ : Y ⟶ X₃) (b : Y ⟶ S) (hg₁ : g₁ ≫ f₁ = b) (hg₂ : g₂ ≫ f₂ = b) (hg₃ : g₃ ≫ f₃ = b) : @@ -221,9 +227,7 @@ lemma isPullback₂ : IsPullback h.p₁₂ h.p₂₃ h₁₂.p₂ h₂₃.p₁ : lemma hom_ext {Y : C} {φ φ' : Y ⟶ h.pullback} (h₁ : φ ≫ h.p₁ = φ' ≫ h.p₁) (h₂ : φ ≫ h.p₂ = φ' ≫ h.p₂) (h₃ : φ ≫ h.p₃ = φ' ≫ h.p₃) : φ = φ' := by - apply h.isPullback₂.hom_ext - · apply h₁₂.isPullback.hom_ext <;> simpa - · apply h₂₃.isPullback.hom_ext <;> simpa + apply h.isPullback₂.hom_ext <;> cat_disch lemma isPullback₁ : IsPullback h.p₁₂ h.p₁₃ h₁₂.p₁ h₁₃.p₁ := .mk' (by simp) (fun _ _ _ h₁ h₂ ↦ h.hom_ext (by simpa using h₁ =≫ h₁₂.p₁) @@ -232,9 +236,7 @@ lemma isPullback₁ : IsPullback h.p₁₂ h.p₁₃ h₁₂.p₁ h₁₃.p₁ : obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ := h.exists_lift (a ≫ h₁₂.p₁) (a ≫ h₁₂.p₂) (b ≫ h₁₃.p₂) _ rfl (by simp) (by simpa using w.symm =≫ f₁) - refine ⟨φ, ?_, ?_⟩ - · apply h₁₂.isPullback.hom_ext <;> simpa - · apply h₁₃.isPullback.hom_ext <;> cat_disch) + exact ⟨φ, by cat_disch, by cat_disch⟩) lemma isPullback₃ : IsPullback h.p₁₃ h.p₂₃ h₁₃.p₂ h₂₃.p₂ := .mk' (by simp) (fun _ _ _ h₁ h₂ ↦ h.hom_ext (by simpa using h₁ =≫ h₁₃.p₁) @@ -243,9 +245,7 @@ lemma isPullback₃ : IsPullback h.p₁₃ h.p₂₃ h₁₃.p₂ h₂₃.p₂ : obtain ⟨φ, hφ₁, hφ₂, hφ₃⟩ := h.exists_lift (a ≫ h₁₃.p₁) (b ≫ h₂₃.p₁) (a ≫ h₁₃.p₂) _ rfl (by simpa using w.symm =≫ f₃) (by simp) - refine ⟨φ, ?_, ?_⟩ - · apply h₁₃.isPullback.hom_ext <;> simpa - · apply h₂₃.isPullback.hom_ext <;> cat_disch) + exact ⟨φ, by cat_disch, by cat_disch⟩) end ChosenPullback₃ From f6ab1f738b45d6d3f34982fd33b74675a0aa6f8f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 17 Feb 2026 19:52:27 +0100 Subject: [PATCH 11/13] IsPushout.mk' --- .../Shapes/Pullback/IsPullback/Basic.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean index 8a0bf56663ecc2..f8719506925fd2 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean @@ -689,6 +689,23 @@ lemma of_isColimit_binaryCofan_of_isInitial · rw [h₁, hc.fac (BinaryCofan.mk s.inr s.inl) ⟨.right⟩] rfl)⟩ +lemma mk' {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} + (hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : P ⟶ T⦄ (_ : inl ≫ φ = inl ≫ φ') + (_ : inr ≫ φ = inr ≫ φ'), φ = φ') + (exists_desc : ∀ ⦃T : C⦄ (a : X ⟶ T) (b : Y ⟶ T) + (_ : f ≫ a = g ≫ b), ∃ (l : P ⟶ T), inl ≫ l = a ∧ inr ≫ l = b) + (w : f ≫ inl = g ≫ inr) : + IsPushout f g inl inr where + w := w + isColimit' := by + let l (s : PushoutCocone f g) := exists_desc _ _ s.condition + exact ⟨PushoutCocone.IsColimit.mk _ + (fun s ↦ (l s).choose) + (fun s ↦ (l s).choose_spec.1) + (fun s ↦ (l s).choose_spec.2) + (fun s m h₁ h₂ ↦ hom_ext + (h₁.trans (l s).choose_spec.1.symm) + (h₂.trans (l s).choose_spec.2.symm))⟩ end IsPushout From d24e78f7ed0a8657405752019428e61c38ef65ad Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 17 Feb 2026 19:53:32 +0100 Subject: [PATCH 12/13] change order --- .../Limits/Shapes/Pullback/IsPullback/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean index f8719506925fd2..414b0f5f2dcf60 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean @@ -690,11 +690,11 @@ lemma of_isColimit_binaryCofan_of_isInitial rfl)⟩ lemma mk' {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} + (w : f ≫ inl = g ≫ inr) (hom_ext : ∀ ⦃T : C⦄ ⦃φ φ' : P ⟶ T⦄ (_ : inl ≫ φ = inl ≫ φ') (_ : inr ≫ φ = inr ≫ φ'), φ = φ') (exists_desc : ∀ ⦃T : C⦄ (a : X ⟶ T) (b : Y ⟶ T) - (_ : f ≫ a = g ≫ b), ∃ (l : P ⟶ T), inl ≫ l = a ∧ inr ≫ l = b) - (w : f ≫ inl = g ≫ inr) : + (_ : f ≫ a = g ≫ b), ∃ (l : P ⟶ T), inl ≫ l = a ∧ inr ≫ l = b) : IsPushout f g inl inr where w := w isColimit' := by From e9c95e3af7683026f5d6e0bacc5a6e2ae2b6dab3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Tue, 17 Feb 2026 20:26:51 +0100 Subject: [PATCH 13/13] fix --- .../Limits/Shapes/Pullback/ChosenPullback.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean index a8f07a05d4f6a6..cdecac8787e192 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/ChosenPullback.lean @@ -83,11 +83,10 @@ namespace LiftStruct attribute [reassoc (attr := simp, grind =)] f_p₁ f_p₂ f_p -variable {h} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} (l : h.LiftStruct g₁ g₂ b) +variable {h} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} -include l in @[reassoc] -lemma w : g₁ ≫ f₁ = g₂ ≫ f₂ := by +lemma w (l : h.LiftStruct g₁ g₂ b) : g₁ ≫ f₁ = g₂ ≫ f₂ := by simp only [← l.f_p₁, ← l.f_p₂, Category.assoc, h.condition] instance : Subsingleton (h.LiftStruct g₁ g₂ b) where @@ -250,3 +249,4 @@ lemma isPullback₃ : IsPullback h.p₁₃ h.p₂₃ h₁₃.p₂ h₂₃.p₂ : end ChosenPullback₃ end CategoryTheory.Limits +#lint