Merge master into nightly-testing

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]

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
 

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

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

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