From 4a7a987ba851b3634c0d6805adf55e34fdb4648f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 27 Sep 2024 21:36:55 +0000 Subject: [PATCH 1/3] feat: add annotations for autolabel workflow (#17188) improve displayed messages --- scripts/autolabel.lean | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/scripts/autolabel.lean b/scripts/autolabel.lean index ccf7d7321c35e..922e98d1fee24 100644 --- a/scripts/autolabel.lean +++ b/scripts/autolabel.lean @@ -239,12 +239,12 @@ to add the label to the PR. - `2`: invalid labels defined - `3`: ~labels do not cover all of `Mathlib/`~ (unused; only emitting warning) -/ -unsafe def main (args : List String): IO Unit := do +unsafe def main (args : List String): IO UInt32 := do if args.length > 1 then println s!"::error:: autolabel: invalid number of arguments ({args.length}), \ expected at most 1. Please run without arguments or provide the target PR's \ number as a single argument!" - IO.Process.exit 1 + return 1 let prNumber? := args[0]? -- test: validate that all paths in `mathlibLabels` actually exist @@ -267,7 +267,7 @@ unsafe def main (args : List String): IO Unit := do Please update `{ ``AutoLabel.mathlibLabels }`!" valid := false unless valid do - IO.Process.exit 2 + return 2 -- test: validate that the labels cover all of the `Mathlib/` folder let notMatchedPaths ← findUncoveredPaths "Mathlib" (exceptions := mathlibUnlabelled) @@ -279,7 +279,7 @@ unsafe def main (args : List String): IO Unit := do s!"Incomplete `{ ``AutoLabel.mathlibLabels }`" s!"the following paths inside `Mathlib/` are not covered \ by any label: {notMatchedPaths} Please modify `AutoLabel.mathlibLabels` accordingly!" - -- IO.Process.exit 3 + -- return 3 -- get the modified files let gitDiff ← IO.Process.run { @@ -290,21 +290,21 @@ unsafe def main (args : List String): IO Unit := do -- find labels covering the modified files let labels := getMatchingLabels modifiedFiles + println s!"::notice::Applicable labels: {labels}" + match labels with | #[] => - println s!"No applicable labels found!" + println s!"::warning::no label to add" | #[label] => - println s!"Exactly one label found: {label}" match prNumber? with | some n => let _ ← IO.Process.run { cmd := "gh", args := #["pr", "edit", n, "--add-label", label] } - println s!"Added label: {label}" + println s!"::notice::added label: {label}" | none => - println s!"No PR-number provided, skipping adding labels. \ + println s!"::warning::no PR-number provided, not adding labels. \ (call `lake exe autolabel 150602` to add the labels to PR `150602`)" - | labels => - println s!"Multiple labels found: {labels}" - println s!"Not adding any label." - IO.Process.exit 0 + | _ => + println s!"::notice::not adding multiple labels: {labels}" + return 0 From 6c1ff14431a4b2fccd3fb3120b80172312e355e1 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Fri, 27 Sep 2024 21:45:34 +0000 Subject: [PATCH 2/3] chore(UniqueProds): fix some `to_additive` names (#17072) --- Mathlib/Algebra/Group/UniqueProds/Basic.lean | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Group/UniqueProds/Basic.lean b/Mathlib/Algebra/Group/UniqueProds/Basic.lean index c243d2138661e..99d252eee8364 100644 --- a/Mathlib/Algebra/Group/UniqueProds/Basic.lean +++ b/Mathlib/Algebra/Group/UniqueProds/Basic.lean @@ -70,13 +70,16 @@ variable {G H : Type*} [Mul G] [Mul H] {A B : Finset G} {a0 b0 : G} theorem of_subsingleton [Subsingleton G] : UniqueMul A B a0 b0 := by simp [UniqueMul, eq_iff_true_of_subsingleton] -@[to_additive] +@[to_additive of_card_le_one] theorem of_card_le_one (hA : A.Nonempty) (hB : B.Nonempty) (hA1 : A.card ≤ 1) (hB1 : B.card ≤ 1) : ∃ a ∈ A, ∃ b ∈ B, UniqueMul A B a b := by rw [Finset.card_le_one_iff] at hA1 hB1 obtain ⟨a, ha⟩ := hA; obtain ⟨b, hb⟩ := hB exact ⟨a, ha, b, hb, fun _ _ ha' hb' _ ↦ ⟨hA1 ha' ha, hB1 hb' hb⟩⟩ +@[deprecated (since := "2024-09-23")] +alias _root_.UniqueAdd.of_card_nonpos := UniqueAdd.of_card_le_one + @[to_additive] theorem mt (h : UniqueMul A B a0 b0) : ∀ ⦃a b⦄, a ∈ A → b ∈ B → a ≠ a0 ∨ b ≠ b0 → a * b ≠ a0 * b0 := fun _ _ ha hb k ↦ by @@ -113,7 +116,7 @@ theorem iff_existsUnique (aA : a0 ∈ A) (bB : b0 ∈ B) : exact Prod.mk.inj_iff.mp (J (x, y) ⟨Finset.mk_mem_product hx hy, l⟩))⟩ open Finset in -@[to_additive] +@[to_additive iff_card_le_one] theorem iff_card_le_one [DecidableEq G] (ha0 : a0 ∈ A) (hb0 : b0 ∈ B) : UniqueMul A B a0 b0 ↔ ((A ×ˢ B).filter (fun p ↦ p.1 * p.2 = a0 * b0)).card ≤ 1 := by simp_rw [card_le_one_iff, mem_filter, mem_product] @@ -124,6 +127,9 @@ theorem iff_card_le_one [DecidableEq G] (ha0 : a0 ∈ A) (hb0 : b0 ∈ B) : · rw [h1.2, h2.2] · exact Prod.ext_iff.1 (@h (a, b) (a0, b0) ⟨⟨ha, hb⟩, he⟩ ⟨⟨ha0, hb0⟩, rfl⟩) +@[deprecated (since := "2024-09-23")] +alias _root_.UniqueAdd.iff_card_nonpos := UniqueAdd.iff_card_le_one + -- Porting note: mathport warning: expanding binder collection -- (ab «expr ∈ » [finset.product/multiset.product/set.prod/list.product](A, B)) -/ @[to_additive] From 2b108d1e9018455f2a4d06b17b06a0f689f42278 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Calle=20S=C3=B6nne?= Date: Fri, 27 Sep 2024 22:13:25 +0000 Subject: [PATCH 3/3] feat(FiberCategory/Fibered): define fibered functors (#12982) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We define the class `IsFibered p`, which captures what it means for a functor `p : 𝒳 ⥤ 𝒮` to be a fibered category, defined as in SGA 1 VI 6.1. We also provide an alternate constructor corresponding to the definition as in [02XM](https://stacks.math.columbia.edu/tag/02XM). Co-authored-by: Paul Lezeau Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com> --- .../FiberedCategory/Cartesian.lean | 38 +++++- .../FiberedCategory/Fibered.lean | 115 +++++++++++++++++- .../FiberedCategory/HomLift.lean | 2 +- 3 files changed, 147 insertions(+), 8 deletions(-) diff --git a/Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean b/Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean index c2f4a20e934c0..b6f222bcedcbc 100644 --- a/Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean +++ b/Mathlib/CategoryTheory/FiberedCategory/Cartesian.lean @@ -119,6 +119,7 @@ lemma map_self : IsCartesian.map p f φ φ = 𝟙 a := by /-- The canonical isomorphism between the domains of two cartesian morphisms lying over the same object. -/ +@[simps] noncomputable def domainUniqueUpToIso {a' : 𝒳} (φ' : a' ⟶ b) [IsCartesian p f φ'] : a' ≅ a where hom := IsCartesian.map p f φ φ' inv := IsCartesian.map p f φ' φ @@ -131,6 +132,14 @@ noncomputable def domainUniqueUpToIso {a' : 𝒳} (φ' : a' ⟶ b) [IsCartesian apply IsCartesian.ext p (p.map φ) φ simp only [assoc, fac, id_comp] +instance domainUniqueUpToIso_inv_isHomLift {a' : 𝒳} (φ' : a' ⟶ b) [IsCartesian p f φ'] : + IsHomLift p (𝟙 R) (domainUniqueUpToIso p f φ φ').hom := + domainUniqueUpToIso_hom p f φ φ' ▸ IsCartesian.map_isHomLift p f φ φ' + +instance domainUniqueUpToIso_hom_isHomLift {a' : 𝒳} (φ' : a' ⟶ b) [IsCartesian p f φ'] : + IsHomLift p (𝟙 R) (domainUniqueUpToIso p f φ φ').inv := + domainUniqueUpToIso_inv p f φ φ' ▸ IsCartesian.map_isHomLift p f φ' φ + /-- Precomposing a cartesian morphism with an isomorphism lifting the identity is cartesian. -/ instance of_iso_comp {a' : 𝒳} (φ' : a' ≅ a) [IsHomLift p (𝟙 R) φ'.hom] : IsCartesian p f (φ'.hom ≫ φ) where @@ -351,15 +360,34 @@ lemma isIso_of_base_isIso (φ : a ⟶ b) [IsStronglyCartesian p f φ] [IsIso f] end +section + +variable {R R' S : 𝒮} {a a' b : 𝒳} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R} + /-- The canonical isomorphism between the domains of two strongly cartesian morphisms lying over isomorphic objects. -/ -noncomputable def domainIsoOfBaseIso {R R' S : 𝒮} {a a' b : 𝒳} {f : R ⟶ S} {f' : R' ⟶ S} - {g : R' ≅ R} (h : f' = g.hom ≫ f) (φ : a ⟶ b) (φ' : a' ⟶ b) [IsStronglyCartesian p f φ] - [IsStronglyCartesian p f' φ'] : a' ≅ a where +@[simps] +noncomputable def domainIsoOfBaseIso (h : f' = g.hom ≫ f) (φ : a ⟶ b) (φ' : a' ⟶ b) + [IsStronglyCartesian p f φ] [IsStronglyCartesian p f' φ'] : a' ≅ a where hom := map p f φ h φ' - inv := by - convert map p f' φ' (congrArg (g.inv ≫ ·) h.symm) φ + inv := + haveI : p.IsHomLift ((fun x ↦ g.inv ≫ x) (g.hom ≫ f)) φ := by + simpa using IsCartesian.toIsHomLift + map p f' φ' (congrArg (g.inv ≫ ·) h.symm) φ + +instance domainUniqueUpToIso_inv_isHomLift (h : f' = g.hom ≫ f) (φ : a ⟶ b) (φ' : a' ⟶ b) + [IsStronglyCartesian p f φ] [IsStronglyCartesian p f' φ'] : + IsHomLift p g.hom (domainIsoOfBaseIso p h φ φ').hom := + domainIsoOfBaseIso_hom p h φ φ' ▸ IsStronglyCartesian.map_isHomLift p f φ h φ' + +instance domainUniqueUpToIso_hom_isHomLift (h : f' = g.hom ≫ f) (φ : a ⟶ b) (φ' : a' ⟶ b) + [IsStronglyCartesian p f φ] [IsStronglyCartesian p f' φ'] : + IsHomLift p g.inv (domainIsoOfBaseIso p h φ φ').inv := by + haveI : p.IsHomLift ((fun x ↦ g.inv ≫ x) (g.hom ≫ f)) φ := by simpa using IsCartesian.toIsHomLift + simpa using IsStronglyCartesian.map_isHomLift p f' φ' (congrArg (g.inv ≫ ·) h.symm) φ + +end end IsStronglyCartesian diff --git a/Mathlib/CategoryTheory/FiberedCategory/Fibered.lean b/Mathlib/CategoryTheory/FiberedCategory/Fibered.lean index c3342d615089e..b826fc429e660 100644 --- a/Mathlib/CategoryTheory/FiberedCategory/Fibered.lean +++ b/Mathlib/CategoryTheory/FiberedCategory/Fibered.lean @@ -17,6 +17,15 @@ This file defines what it means for a functor `p : 𝒳 ⥤ 𝒮` to be (pre)fib - `IsPreFibered p` expresses `𝒳` is fibered over `𝒮` via a functor `p : 𝒳 ⥤ 𝒮`, as in SGA VI.6.1. This means that any morphism in the base `𝒮` can be lifted to a cartesian morphism in `𝒳`. +- `IsFibered p` expresses `𝒳` is fibered over `𝒮` via a functor `p : 𝒳 ⥤ 𝒮`, as in SGA VI.6.1. +This means that it is prefibered, and that the composition of any two cartesian morphisms is +cartesian. + +In the literature one often sees the notion of a fibered category defined as the existence of +strongly cartesian morphisms lying over any given morphism in the base. This is equivalent to the +notion above, and we give an alternate constructor `IsFibered.of_exists_isCartesian'` for +constructing a fibered category this way. + ## Implementation The constructor of `IsPreFibered` is called `exists_isCartesian'`. The reason for the prime is that @@ -47,7 +56,18 @@ protected lemma IsPreFibered.exists_isCartesian (p : 𝒳 ⥤ 𝒮) [p.IsPreFibe (ha : p.obj a = S) (f : R ⟶ S) : ∃ (b : 𝒳) (φ : b ⟶ a), IsCartesian p f φ := by subst ha; exact IsPreFibered.exists_isCartesian' f -namespace IsPreFibered +/-- Definition of a fibered category. + +See SGA 1 VI.6.1. -/ +class Functor.IsFibered (p : 𝒳 ⥤ 𝒮) extends IsPreFibered p : Prop where + comp {R S T : 𝒮} (f : R ⟶ S) (g : S ⟶ T) {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c) + [IsCartesian p f φ] [IsCartesian p g ψ] : IsCartesian p (f ≫ g) (φ ≫ ψ) + +instance (p : 𝒳 ⥤ 𝒮) [p.IsFibered] {R S T : 𝒮} (f : R ⟶ S) (g : S ⟶ T) {a b c : 𝒳} (φ : a ⟶ b) + (ψ : b ⟶ c) [IsCartesian p f φ] [IsCartesian p g ψ] : IsCartesian p (f ≫ g) (φ ≫ ψ) := + IsFibered.comp f g φ ψ + +namespace Functor.IsPreFibered open IsCartesian @@ -70,6 +90,97 @@ instance pullbackMap.IsCartesian : IsCartesian p f (pullbackMap ha f) := lemma pullbackObj_proj : p.obj (pullbackObj ha f) = R := domain_eq p f (pullbackMap ha f) -end IsPreFibered +end Functor.IsPreFibered + +namespace Functor.IsFibered + +open IsCartesian IsPreFibered + +/-- In a fibered category, any cartesian morphism is strongly cartesian. -/ +instance isStronglyCartesian_of_isCartesian (p : 𝒳 ⥤ 𝒮) [p.IsFibered] {R S : 𝒮} (f : R ⟶ S) + {a b : 𝒳} (φ : a ⟶ b) [p.IsCartesian f φ] : p.IsStronglyCartesian f φ where + universal_property' g φ' hφ' := by + -- Let `ψ` be a cartesian arrow lying over `g` + let ψ := pullbackMap (domain_eq p f φ) g + -- Let `τ` be the map induced by the universal property of `ψ ≫ φ`. + let τ := IsCartesian.map p (g ≫ f) (ψ ≫ φ) φ' + use τ ≫ ψ + -- It is easily verified that `τ ≫ ψ` lifts `g` and `τ ≫ ψ ≫ φ = φ'` + refine ⟨⟨inferInstance, by simp only [assoc, IsCartesian.fac, τ]⟩, ?_⟩ + -- It remains to check that `τ ≫ ψ` is unique. + -- So fix another lift `π` of `g` satisfying `π ≫ φ = φ'`. + intro π ⟨hπ, hπ_comp⟩ + -- Write `π` as `π = τ' ≫ ψ` for some `τ'` induced by the universal property of `ψ`. + rw [← fac p g ψ π] + -- It remains to show that `τ' = τ`. This follows again from the universal property of `ψ`. + congr 1 + apply map_uniq + rwa [← assoc, IsCartesian.fac] + +/-- In a category which admits strongly cartesian pullbacks, any cartesian morphism is +strongly cartesian. This is a helper-lemma for the fact that admitting strongly cartesian pullbacks +implies being fibered. -/ +lemma isStronglyCartesian_of_exists_isCartesian (p : 𝒳 ⥤ 𝒮) (h : ∀ (a : 𝒳) (R : 𝒮) + (f : R ⟶ p.obj a), ∃ (b : 𝒳) (φ : b ⟶ a), IsStronglyCartesian p f φ) {R S : 𝒮} (f : R ⟶ S) + {a b : 𝒳} (φ : a ⟶ b) [p.IsCartesian f φ] : p.IsStronglyCartesian f φ := by + constructor + intro c g φ' hφ' + subst_hom_lift p f φ; clear a b R S + -- Let `ψ` be a cartesian arrow lying over `g` + obtain ⟨a', ψ, hψ⟩ := h _ _ (p.map φ) + -- Let `τ' : c ⟶ a'` be the map induced by the universal property of `ψ` + let τ' := IsStronglyCartesian.map p (p.map φ) ψ (f':= g ≫ p.map φ) rfl φ' + -- Let `Φ : a' ≅ a` be natural isomorphism induced between `φ` and `ψ`. + let Φ := domainUniqueUpToIso p (p.map φ) φ ψ + -- The map induced by `φ` will be `τ' ≫ Φ.hom` + use τ' ≫ Φ.hom + -- It is easily verified that `τ' ≫ Φ.hom` lifts `g` and `τ' ≫ Φ.hom ≫ φ = φ'` + refine ⟨⟨by simp only [Φ]; infer_instance, ?_⟩, ?_⟩ + · simp [τ', Φ, IsStronglyCartesian.map_uniq p (p.map φ) ψ rfl φ'] + -- It remains to check that it is unique. This follows from the universal property of `ψ`. + intro π ⟨hπ, hπ_comp⟩ + rw [← Iso.comp_inv_eq] + apply IsStronglyCartesian.map_uniq p (p.map φ) ψ rfl φ' + simp [hπ_comp, Φ] + +/-- Alternate constructor for `IsFibered`, a functor `p : 𝒳 ⥤ 𝒴` is fibered if any diagram of the +form +``` + a + - + | + v +R --f--> p(a) +``` +admits a strongly cartesian lift `b ⟶ a` of `f`. -/ +lemma of_exists_isStronglyCartesian {p : 𝒳 ⥤ 𝒮} + (h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), + ∃ (b : 𝒳) (φ : b ⟶ a), IsStronglyCartesian p f φ) : + IsFibered p where + exists_isCartesian' := by + intro a R f + obtain ⟨b, φ, hφ⟩ := h a R f + refine ⟨b, φ, inferInstance⟩ + comp := fun R S T f g {a b c} φ ψ _ _ => + have : p.IsStronglyCartesian f φ := isStronglyCartesian_of_exists_isCartesian p h _ _ + have : p.IsStronglyCartesian g ψ := isStronglyCartesian_of_exists_isCartesian p h _ _ + inferInstance + +/-- Given a diagram +``` + a + - + | + v +T --g--> R --f--> S +``` +we have an isomorphism `T ×_S a ≅ T ×_R (R ×_S a)` -/ +noncomputable def pullbackPullbackIso {p : 𝒳 ⥤ 𝒮} [IsFibered p] + {R S T : 𝒮} {a : 𝒳} (ha : p.obj a = S) (f : R ⟶ S) (g : T ⟶ R) : + pullbackObj ha (g ≫ f) ≅ pullbackObj (pullbackObj_proj ha f) g := + domainUniqueUpToIso p (g ≫ f) (pullbackMap (pullbackObj_proj ha f) g ≫ pullbackMap ha f) + (pullbackMap ha (g ≫ f)) + +end Functor.IsFibered end CategoryTheory diff --git a/Mathlib/CategoryTheory/FiberedCategory/HomLift.lean b/Mathlib/CategoryTheory/FiberedCategory/HomLift.lean index 595fb845dc473..8de8bf2c92401 100644 --- a/Mathlib/CategoryTheory/FiberedCategory/HomLift.lean +++ b/Mathlib/CategoryTheory/FiberedCategory/HomLift.lean @@ -142,7 +142,7 @@ instance comp_lift_id_left {a b c : 𝒳} {S T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ lemma comp_lift_id_left' {a b c : 𝒳} (R : 𝒮) (φ : a ⟶ b) [p.IsHomLift (𝟙 R) φ] {S T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ c) [p.IsHomLift f ψ] : p.IsHomLift f (φ ≫ ψ) := by obtain rfl : R = S := by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ] - simpa using inferInstanceAs (p.IsHomLift (𝟙 R ≫ f) (φ ≫ ψ)) + infer_instance lemma eqToHom_domain_lift_id {p : 𝒳 ⥤ 𝒮} {a b : 𝒳} (hab : a = b) {R : 𝒮} (hR : p.obj a = R) : p.IsHomLift (𝟙 R) (eqToHom hab) := by