chore(CategoryTheory/Sites): generalize universes in Sheaf.isSheaf_of_isRepresentable (leanprover-community#34234)

For this we add some API on representable functors.

Author: chrisflav

Mathlib/Algebra/Category/Grp/Ulift.lean

@@ -103,8 +103,8 @@ instance : uliftFunctor.{u, v}.Full := uliftFunctorFullyFaithful.full
 @[to_additive]
 noncomputable instance uliftFunctor_preservesLimit {J : Type w} [Category.{w'} J]
     (K : J ⥤ GrpCat.{u}) : PreservesLimit K uliftFunctor.{v, u} where
-  preserves lc := ⟨isLimitOfReflects (forget GrpCat.{max u v})
-    (isLimitOfPreserves CategoryTheory.uliftFunctor (isLimitOfPreserves (forget GrpCat) lc))⟩
+  preserves lc := ⟨isLimitOfReflects (forget GrpCat) <|
+    isLimitOfPreserves CategoryTheory.uliftFunctor.{v} (isLimitOfPreserves (forget GrpCat) lc)⟩
 
 @[to_additive]
 noncomputable instance uliftFunctor_preservesLimitsOfShape {J : Type w} [Category.{w'} J] :
@@ -153,8 +153,8 @@ instance : uliftFunctor.{u, v}.Full := uliftFunctorFullyFaithful.full
 @[to_additive]
 noncomputable instance uliftFunctor_preservesLimit {J : Type w} [Category.{w'} J]
     (K : J ⥤ CommGrpCat.{u}) : PreservesLimit K uliftFunctor.{v, u} where
-  preserves lc := ⟨isLimitOfReflects (forget CommGrpCat.{max u v})
-    (isLimitOfPreserves CategoryTheory.uliftFunctor (isLimitOfPreserves (forget CommGrpCat) lc))⟩
+  preserves lc := ⟨isLimitOfReflects (forget CommGrpCat) <|
+    isLimitOfPreserves CategoryTheory.uliftFunctor.{v} (isLimitOfPreserves (forget CommGrpCat) lc)⟩
 
 @[to_additive]
 noncomputable instance uliftFunctor_preservesLimitsOfShape {J : Type w} [Category.{w'} J] :

Mathlib/CategoryTheory/Sites/Canonical.lean

@@ -195,9 +195,14 @@ theorem isSheaf_yoneda_obj (X : C) : Presieve.IsSheaf (canonicalTopology C) (yon
   fun _ _ hS => sheaf_for_finestTopology _ (Set.mem_range_self _) _ hS
 
 /-- A representable functor is a sheaf for the canonical topology. -/
-theorem isSheaf_of_isRepresentable (P : Cᵒᵖ ⥤ Type v) [P.IsRepresentable] :
-    Presieve.IsSheaf (canonicalTopology C) P :=
-  Presieve.isSheaf_iso (canonicalTopology C) P.reprW (isSheaf_yoneda_obj _)
+theorem isSheaf_of_isRepresentable (P : Cᵒᵖ ⥤ Type w) [P.IsRepresentable] :
+    Presieve.IsSheaf (canonicalTopology C) P := by
+  rw [← Presieve.isSheaf_comp_uliftFunctor_iff]
+  refine Presieve.isSheaf_iso (canonicalTopology C) (P ⋙ uliftFunctor.{v}).uliftYonedaReprXIso ?_
+  rw [← isSheaf_iff_isSheaf_of_type]
+  refine GrothendieckTopology.HasSheafCompose.isSheaf _ ?_
+  rw [isSheaf_iff_isSheaf_of_type]
+  exact isSheaf_yoneda_obj _
 
 end Sheaf
 
@@ -226,7 +231,7 @@ theorem of_isSheaf_yoneda_obj (J : GrothendieckTopology C)
 
 /-- If `J` is subcanonical, then any representable is a `J`-sheaf. -/
 theorem isSheaf_of_isRepresentable {J : GrothendieckTopology C} [Subcanonical J]
-    (P : Cᵒᵖ ⥤ Type v) [P.IsRepresentable] : Presieve.IsSheaf J P :=
+    (P : Cᵒᵖ ⥤ Type w) [P.IsRepresentable] : Presieve.IsSheaf J P :=
   Presieve.isSheaf_of_le _ J.le_canonical (Sheaf.isSheaf_of_isRepresentable P)
 
 end Subcanonical

Mathlib/CategoryTheory/Sites/SheafOfTypes.lean

@@ -160,9 +160,14 @@ theorem isSheaf_pretopology [HasPullbacks C] (K : Pretopology C) :
 theorem isSheaf_bot : IsSheaf (⊥ : GrothendieckTopology C) P := fun X => by
   simp [isSheafFor_top]
 
+/-- A presheaf is a sheaf after composiing with a universe lift if and only if it is a sheaf. -/
+@[simp]
+theorem isSheaf_comp_uliftFunctor_iff : IsSheaf J (P ⋙ uliftFunctor.{w'}) ↔ IsSheaf J P :=
+  (isSheaf_iff_of_nat_equiv (fun _ => Equiv.ulift.symm) (fun _ _ _ _ => rfl)).symm
+
 /-- The composition of a sheaf with a ULift functor is still a sheaf. -/
-theorem isSheaf_comp_uliftFunctor (h : IsSheaf J P) : IsSheaf J (P ⋙ uliftFunctor.{w'}) :=
-  isSheaf_of_nat_equiv (fun _ => Equiv.ulift.symm) (fun _ _ _ _ => rfl) h
+theorem isSheaf_comp_uliftFunctor (h : IsSheaf J P) : IsSheaf J (P ⋙ uliftFunctor.{w'}) := by
+  rwa [isSheaf_comp_uliftFunctor_iff]
 
 /--
 For a presheaf of the form `yoneda.obj W`, a compatible family of elements on a sieve

Mathlib/CategoryTheory/Yoneda.lean

@@ -533,6 +533,17 @@ theorem reprW_hom_app (F : Cᵒᵖ ⥤ Type v₁) [F.IsRepresentable]
     F.reprW.hom.app X f = F.map f.op F.reprx := by
   apply RepresentableBy.homEquiv_eq
 
+/-- If `F` is representable, it is, modulo universe lifting, isomorphic to
+`Hom(-, X)` for the representing object `X`. -/
+noncomputable def uliftYonedaReprXIso (F : Cᵒᵖ ⥤ Type (max v v₁)) [F.IsRepresentable] :
+    uliftYoneda.{v}.obj F.reprX ≅ F :=
+  (RepresentableBy.equivUliftYonedaIso F _) F.representableBy
+
+lemma uliftYonedaReprXIso_hom_app (F : Cᵒᵖ ⥤ Type (max v v₁)) [F.IsRepresentable]
+    (X : Cᵒᵖ) (f : ULift (unop X ⟶ F.reprX)) :
+    F.uliftYonedaReprXIso.hom.app X f = F.map f.down.op F.reprx :=
+  RepresentableBy.homEquiv_eq _ _
+
 end Representable
 
 section Corepresentable
@@ -571,6 +582,17 @@ theorem coreprW_hom_app (F : C ⥤ Type v₁) [F.IsCorepresentable] (X : C) (f :
     F.coreprW.hom.app X f = F.map f F.coreprx := by
   apply CorepresentableBy.homEquiv_eq
 
+/-- If `F` is corepresentable, it is, modulo universe lifting, isomorphic to
+`Hom(X, -)` for the corepresenting object `X`. -/
+noncomputable def uliftCoyonedaCoreprXIso (F : C ⥤ Type (max v v₁)) [F.IsCorepresentable] :
+    uliftCoyoneda.{v}.obj (op F.coreprX) ≅ F :=
+  (CorepresentableBy.equivUliftCoyonedaIso F _) F.corepresentableBy
+
+lemma uliftCoyonedaCoreprXIso_hom_app (F : C ⥤ Type (max v v₁)) [F.IsCorepresentable]
+    (X : C) (f : ULift (F.coreprX ⟶ X)) :
+    F.uliftCoyonedaCoreprXIso.hom.app X f = F.map f.down F.coreprx :=
+  CorepresentableBy.homEquiv_eq _ _
+
 end Corepresentable
 
 lemma isRepresentable_comp_uliftFunctor_iff {F : Cᵒᵖ ⥤ Type v} :
@@ -583,6 +605,12 @@ lemma isCorepresentable_comp_uliftFunctor_iff {F : C ⥤ Type v} :
   mp | ⟨X, ⟨R⟩⟩ => ⟨X, ⟨corepresentableByUliftFunctorEquiv R⟩⟩
   mpr | ⟨X, ⟨R⟩⟩ => ⟨X, ⟨corepresentableByUliftFunctorEquiv.symm R⟩⟩
 
+instance (F : Cᵒᵖ ⥤ Type v) [F.IsRepresentable] : (F ⋙ uliftFunctor.{w}).IsRepresentable :=
+  isRepresentable_comp_uliftFunctor_iff.mpr ‹_›
+
+instance (F : C ⥤ Type v) [F.IsCorepresentable] : (F ⋙ uliftFunctor.{w}).IsCorepresentable :=
+  isCorepresentable_comp_uliftFunctor_iff.mpr ‹_›
+
 end Functor
 
 theorem isRepresentable_of_natIso (F : Cᵒᵖ ⥤ Type v₁) {G} (i : F ≅ G) [F.IsRepresentable] :