chore(CategoryTheory/Limits/Concrete): generalize universe assumptions (

#10418)

Generalizes universe assumptions for various statements on colimits in concrete categories. Also simplifies some proofs.

Mathlib/Algebra/Category/GroupCat/Abelian.lean

@@ -69,7 +69,8 @@ instance {J : Type u} [SmallCategory J] [IsFiltered J] :
     rcases Concrete.colimit_exists_rep G x with ⟨j, y, rfl⟩
     erw [← comp_apply, colimit.ι_map, comp_apply,
       ← map_zero (by exact colimit.ι H j : H.obj j →+ ↑(colimit H))] at hx
-    rcases Concrete.colimit_exists_of_rep_eq H _ _ hx with ⟨k, e₁, e₂, hk : _ = H.map e₂ 0⟩
+    rcases Concrete.colimit_exists_of_rep_eq.{u} H _ _ hx with
+      ⟨k, e₁, e₂, hk : _ = H.map e₂ 0⟩
     rw [map_zero, ← comp_apply, ← NatTrans.naturality, comp_apply] at hk
     rcases ((exact_iff _ _).mp <| h k).ge hk with ⟨t, ht⟩
     use colimit.ι F k t

Mathlib/CategoryTheory/Limits/ConcreteCategory.lean

@@ -15,7 +15,7 @@ import Mathlib.Tactic.ApplyFun
 -/
 
 
-universe w v u
+universe t w v u r
 
 open CategoryTheory
 
@@ -58,33 +58,19 @@ end Limits
 
 section Colimits
 
-variable {C : Type u} [Category.{v} C] [ConcreteCategory.{v} C] {J : Type v} [SmallCategory J]
+section
+
+variable {C : Type u} [Category.{v} C] [ConcreteCategory.{t} C] {J : Type w} [Category.{r} J]
   (F : J ⥤ C) [PreservesColimit F (forget C)]
 
 theorem Concrete.from_union_surjective_of_isColimit {D : Cocone F} (hD : IsColimit D) :
     let ff : (Σj : J, F.obj j) → D.pt := fun a => D.ι.app a.1 a.2
     Function.Surjective ff := by
-  intro ff
-  let E := (forget C).mapCocone D
-  let hE : IsColimit E := isColimitOfPreserves _ hD
-  let G := Types.colimitCocone.{v, v} (F ⋙ forget C)
-  let hG := Types.colimitCoconeIsColimit.{v, v} (F ⋙ forget C)
-  let T : E ≅ G := hE.uniqueUpToIso hG
-  let TX : E.pt ≅ G.pt := (Cocones.forget _).mapIso T
-  suffices Function.Surjective (TX.hom ∘ ff) by
-    intro a
-    obtain ⟨b, hb⟩ := this (TX.hom a)
-    refine' ⟨b, _⟩
-    apply_fun TX.inv at hb
-    change (TX.hom ≫ TX.inv) (ff b) = (TX.hom ≫ TX.inv) _ at hb
-    simpa only [TX.hom_inv_id] using hb
-  have : TX.hom ∘ ff = fun a => G.ι.app a.1 a.2 := by
-    ext a
-    change (E.ι.app a.1 ≫ hE.desc G) a.2 = _
-    rw [hE.fac]
-  rw [this]
-  rintro ⟨⟨j, a⟩⟩
-  exact ⟨⟨j, a⟩, rfl⟩
+  intro ff x
+  let E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
+  let hE : IsColimit E := isColimitOfPreserves (forget C) hD
+  obtain ⟨j, y, hy⟩ := Types.jointly_surjective_of_isColimit hE x
+  exact ⟨⟨j, y⟩, hy⟩
 #align category_theory.limits.concrete.from_union_surjective_of_is_colimit CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit
 
 theorem Concrete.isColimit_exists_rep {D : Cocone F} (hD : IsColimit D) (x : D.pt) :
@@ -98,92 +84,55 @@ theorem Concrete.colimit_exists_rep [HasColimit F] (x : ↑(colimit F)) :
   Concrete.isColimit_exists_rep F (colimit.isColimit _) x
 #align category_theory.limits.concrete.colimit_exists_rep CategoryTheory.Limits.Concrete.colimit_exists_rep
 
-theorem Concrete.isColimit_rep_eq_of_exists {D : Cocone F} {i j : J} (hD : IsColimit D)
-    (x : F.obj i) (y : F.obj j) (h : ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y) :
+theorem Concrete.isColimit_rep_eq_of_exists {D : Cocone F} {i j : J} (x : F.obj i) (y : F.obj j)
+    (h : ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y) :
     D.ι.app i x = D.ι.app j y := by
   let E := (forget C).mapCocone D
-  let hE : IsColimit E := isColimitOfPreserves _ hD
-  let G := Types.colimitCocone.{v, v} (F ⋙ forget C)
-  let hG := Types.colimitCoconeIsColimit.{v, v} (F ⋙ forget C)
-  let T : E ≅ G := hE.uniqueUpToIso hG
-  let TX : E.pt ≅ G.pt := (Cocones.forget _).mapIso T
-  apply_fun TX.hom using injective_of_mono TX.hom
-  change (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y
-  erw [T.hom.w, T.hom.w]
-  obtain ⟨k, f, g, h⟩ := h
-  have : G.ι.app i x = (G.ι.app k (F.map f x) : G.pt) := Quot.sound ⟨f, rfl⟩
-  rw [this, h]
-  symm
-  exact Quot.sound ⟨g, rfl⟩
+  obtain ⟨k, f, g, (hfg : (F ⋙ forget C).map f x = F.map g y)⟩ := h
+  let h1 : (F ⋙ forget C).map f ≫ E.ι.app k = E.ι.app i := E.ι.naturality f
+  let h2 : (F ⋙ forget C).map g ≫ E.ι.app k = E.ι.app j := E.ι.naturality g
+  show E.ι.app i x = E.ι.app j y
+  rw [← h1, types_comp_apply, hfg]
+  exact congrFun h2 y
 #align category_theory.limits.concrete.is_colimit_rep_eq_of_exists CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists
 
 theorem Concrete.colimit_rep_eq_of_exists [HasColimit F] {i j : J} (x : F.obj i) (y : F.obj j)
     (h : ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y) :
     colimit.ι F i x = colimit.ι F j y :=
-  Concrete.isColimit_rep_eq_of_exists F (colimit.isColimit _) x y h
+  Concrete.isColimit_rep_eq_of_exists F x y h
 #align category_theory.limits.concrete.colimit_rep_eq_of_exists CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists
 
+end
+
 section FilteredColimits
 
-variable [IsFiltered J]
+variable {C : Type u} [Category.{v} C] [ConcreteCategory.{max t w} C] {J : Type w} [Category.{r} J]
+  (F : J ⥤ C) [PreservesColimit F (forget C)] [IsFiltered J]
 
 theorem Concrete.isColimit_exists_of_rep_eq {D : Cocone F} {i j : J} (hD : IsColimit D)
     (x : F.obj i) (y : F.obj j) (h : D.ι.app _ x = D.ι.app _ y) :
     ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y := by
   let E := (forget C).mapCocone D
   let hE : IsColimit E := isColimitOfPreserves _ hD
-  let G := Types.colimitCocone.{v, v} (F ⋙ forget C)
-  let hG := Types.colimitCoconeIsColimit.{v, v} (F ⋙ forget C)
-  let T : E ≅ G := hE.uniqueUpToIso hG
-  let TX : E.pt ≅ G.pt := (Cocones.forget _).mapIso T
-  apply_fun TX.hom at h
-  change (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y at h
-  erw [T.hom.w, T.hom.w] at h
-  replace h := Quot.exact _ h
-  suffices
-    ∀ (a b : Σj, F.obj j) (_ : EqvGen (Limits.Types.Quot.Rel.{v, v} (F ⋙ forget C)) a b),
-      ∃ (k : _) (f : a.1 ⟶ k) (g : b.1 ⟶ k), F.map f a.2 = F.map g b.2
-    by exact this ⟨i, x⟩ ⟨j, y⟩ h
-  intro a b h
-  induction h with
-  | rel x y hh =>
-    obtain ⟨e, he⟩ := hh
-    use y.1, e, 𝟙 _
-    simpa using he.symm
-  | refl x =>
-    exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
-  | symm x y _ hh =>
-    obtain ⟨k, f, g, hh⟩ := hh
-    exact ⟨k, g, f, hh.symm⟩
-  | trans x y z _ _ hh1 hh2 =>
-    obtain ⟨k1, f1, g1, h1⟩ := hh1
-    obtain ⟨k2, f2, g2, h2⟩ := hh2
-    let k0 : J := IsFiltered.max k1 k2
-    let e1 : k1 ⟶ k0 := IsFiltered.leftToMax _ _
-    let e2 : k2 ⟶ k0 := IsFiltered.rightToMax _ _
-    let k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
-    let e : k0 ⟶ k := IsFiltered.coeqHom _ _
-    use k, f1 ≫ e1 ≫ e, g2 ≫ e2 ≫ e
-    simp only [F.map_comp, comp_apply, h1, ← h2]
-    simp only [← comp_apply, ← F.map_comp]
-    rw [IsFiltered.coeq_condition]
+  exact (Types.FilteredColimit.isColimit_eq_iff.{w, t, r} (F ⋙ forget C) hE).mp h
 #align category_theory.limits.concrete.is_colimit_exists_of_rep_eq CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq
 
 theorem Concrete.isColimit_rep_eq_iff_exists {D : Cocone F} {i j : J} (hD : IsColimit D)
     (x : F.obj i) (y : F.obj j) :
     D.ι.app i x = D.ι.app j y ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y :=
-  ⟨Concrete.isColimit_exists_of_rep_eq _ hD _ _, Concrete.isColimit_rep_eq_of_exists _ hD _ _⟩
+  ⟨Concrete.isColimit_exists_of_rep_eq.{t} _ hD _ _,
+   Concrete.isColimit_rep_eq_of_exists _ _ _⟩
 #align category_theory.limits.concrete.is_colimit_rep_eq_iff_exists CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists
 
 theorem Concrete.colimit_exists_of_rep_eq [HasColimit F] {i j : J} (x : F.obj i) (y : F.obj j)
     (h : colimit.ι F _ x = colimit.ι F _ y) :
     ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y :=
-  Concrete.isColimit_exists_of_rep_eq F (colimit.isColimit _) x y h
+  Concrete.isColimit_exists_of_rep_eq.{t} F (colimit.isColimit _) x y h
 #align category_theory.limits.concrete.colimit_exists_of_rep_eq CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq
 
 theorem Concrete.colimit_rep_eq_iff_exists [HasColimit F] {i j : J} (x : F.obj i) (y : F.obj j) :
     colimit.ι F i x = colimit.ι F j y ↔ ∃ (k : _) (f : i ⟶ k) (g : j ⟶ k), F.map f x = F.map g y :=
-  ⟨Concrete.colimit_exists_of_rep_eq _ _ _, Concrete.colimit_rep_eq_of_exists _ _ _⟩
+  ⟨Concrete.colimit_exists_of_rep_eq.{t} _ _ _, Concrete.colimit_rep_eq_of_exists _ _ _⟩
 #align category_theory.limits.concrete.colimit_rep_eq_iff_exists CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists
 
 end FilteredColimits

Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean

@@ -241,7 +241,7 @@ theorem eq_mk_iff_exists {X : C} {P : Cᵒᵖ ⥤ D} {S T : J.Cover X} (x : Meq
     mk x = mk y ↔ ∃ (W : J.Cover X) (h1 : W ⟶ S) (h2 : W ⟶ T), x.refine h1 = y.refine h2 := by
   constructor
   · intro h
-    obtain ⟨W, h1, h2, hh⟩ := Concrete.colimit_exists_of_rep_eq _ _ _ h
+    obtain ⟨W, h1, h2, hh⟩ := Concrete.colimit_exists_of_rep_eq.{u} _ _ _ h
     use W.unop, h1.unop, h2.unop
     ext I
     apply_fun Multiequalizer.ι (W.unop.index P) I at hh