refactor(CategoryTheory): redefine MorphismProperty.IsLocalAtTarget in terms of presieves (#39978)

This changes the definition slightly: The condition is now required for covers indexed in `Type max u v`, while before this PR it was only required for index types in `Type v`.

Requested in review of #32046.

Author: chrisflav

Mathlib/AlgebraicGeometry/Cover/Open.lean

@@ -62,19 +62,19 @@ def affineCover (X : Scheme.{u}) : OpenCover X := by
 instance : Inhabited X.OpenCover :=
   ⟨X.affineCover⟩
 
-theorem OpenCover.iSup_opensRange {X : Scheme.{u}} (𝒰 : X.OpenCover) :
+theorem OpenCover.iSup_opensRange {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X) :
     ⨆ i, (𝒰.f i).opensRange = ⊤ :=
   Opens.ext <| by rw [Opens.coe_iSup]; exact 𝒰.iUnion_range
 
 /-- The ranges of the maps in a scheme-theoretic open cover are a topological open cover. -/
-lemma OpenCover.isOpenCover_opensRange {X : Scheme.{u}} (𝒰 : X.OpenCover) :
+lemma OpenCover.isOpenCover_opensRange {X : Scheme.{u}} (𝒰 : OpenCover.{v} X) :
     IsOpenCover fun i ↦ (𝒰.f i).opensRange :=
   .mk 𝒰.iSup_opensRange
 
 /-- Every open cover of a quasi-compact scheme can be refined into a finite subcover.
 -/
 @[simps! X f]
-def OpenCover.finiteSubcover {X : Scheme.{u}} (𝒰 : OpenCover X) [H : CompactSpace X] :
+def OpenCover.finiteSubcover {X : Scheme.{u}} (𝒰 : OpenCover.{v} X) [H : CompactSpace X] :
     OpenCover X := by
   have :=
     @CompactSpace.elim_nhds_subcover _ _ H (fun x : X => Set.range (𝒰.f (𝒰.idx x)))

Mathlib/AlgebraicGeometry/Morphisms/Basic.lean

@@ -125,11 +125,12 @@ protected lemma mk' {P : MorphismProperty Scheme} [P.RespectsIso]
     (of_sSup_eq_top :
       ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ →
         (∀ i, P (f ∣_ U i)) → P f) :
-    IsZariskiLocalAtTarget P where
-  pullbackSnd 𝒰 i hf := (P.arrow_mk_iso_iff (morphismRestrictOpensRange _ _)).mp (restrict _ _ hf)
-  of_zeroHypercover {X Y f} 𝒰 h := by
-    refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) ?_
-    exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h i)
+    IsZariskiLocalAtTarget P := by
+  refine .mk_of_iff_of_zeroHypercover fun {X Y} f 𝒰 ↦ ?_
+  refine ⟨fun hf i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange _ _)).mp (restrict _ _ hf),
+    fun h ↦ ?_⟩
+  refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange <| .ulift 𝒰) ?_
+  exact fun i ↦ (P.arrow_mk_iso_iff (morphismRestrictOpensRange f _)).mpr (h _)
 
 variable {P : MorphismProperty Scheme.{u}} [IsZariskiLocalAtTarget P]
   {X Y : Scheme.{u}} {f : X ⟶ Y} (𝒰 : Y.OpenCover)
@@ -233,18 +234,18 @@ protected lemma mk' {P : MorphismProperty Scheme} [P.RespectsIso]
     (of_sSup_eq_top :
       ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ →
         (∀ i, P ((U i).ι ≫ f)) → P f) :
-    IsZariskiLocalAtSource P where
-  comp 𝒰 i H := by
-    rw [← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
+    IsZariskiLocalAtSource P := by
+  refine .mk_of_iff_of_zeroHypercover fun {X Y} f 𝒰 ↦ ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩
+  · rw [← IsOpenImmersion.isoOfRangeEq_hom_fac (𝒰.f i) (Scheme.Opens.ι _)
       (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
       P.cancel_left_of_respectsIso]
-    exact restrict _ _ H
-  of_zeroHypercover {X Y} f 𝒰 h := by
-    refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange 𝒰) fun i ↦ ?_
-    rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f i) (Scheme.Opens.ι _)
-      (congr_arg Opens.carrier (𝒰.f i).opensRange.opensRange_ι.symm), Category.assoc,
+    exact restrict _ _ hf
+  · refine of_sSup_eq_top f _ (Scheme.OpenCover.iSup_opensRange <| .ulift 𝒰) fun i ↦ ?_
+    dsimp
+    rw [← IsOpenImmersion.isoOfRangeEq_inv_fac (𝒰.f _) (Scheme.Opens.ι _)
+      (congr_arg Opens.carrier (𝒰.f _).opensRange.opensRange_ι.symm), Category.assoc,
       P.cancel_left_of_respectsIso]
-    exact h _
+    exact hf _
 
 variable {P : MorphismProperty Scheme.{u}} [IsZariskiLocalAtSource P]
 variable {X Y : Scheme.{u}} {f : X ⟶ Y} (𝒰 : X.OpenCover)
@@ -286,13 +287,12 @@ lemma of_isOpenImmersion [P.ContainsIdentities] [IsOpenImmersion f] : P f :=
 
 lemma isZariskiLocalAtTarget [P.IsMultiplicative]
     (hP : ∀ {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion g], P (f ≫ g) → P f) :
-    IsZariskiLocalAtTarget P where
-  pullbackSnd {X Y} f 𝒰 i hf := by
-    apply hP _ (𝒰.f i)
+    IsZariskiLocalAtTarget P := by
+  refine .mk_of_iff_of_zeroHypercover fun {X Y} f 𝒰 ↦ ⟨fun hf i ↦ ?_, fun h ↦ ?_⟩
+  · apply hP _ (𝒰.f i)
     rw [← pullback.condition]
     exact IsZariskiLocalAtSource.comp hf _
-  of_zeroHypercover {X Y} f 𝒰 h := by
-    rw [P.iff_of_zeroHypercover_source (𝒰.pullback₁ f)]
+  · rw [P.iff_of_zeroHypercover_source (𝒰.pullback₁ f)]
     intro i
     rw [← Scheme.Cover.pullbackHom_map]
     exact P.comp_mem _ _ (h i) (of_isOpenImmersion _)
@@ -646,13 +646,16 @@ theorem isStableUnderBaseChange (hP' : Q.IsStableUnderBaseChange) :
 lemma isZariskiLocalAtSource
     (H : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine Y] (𝒰 : Scheme.OpenCover.{u} X),
         Q f ↔ ∀ i, Q (𝒰.f i ≫ f)) : IsZariskiLocalAtSource P := by
-  refine .mk_of_iff ?_
-  intro X Y f 𝒰
-  simp_rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top _ (iSup_affineOpens_eq_top Y)]
-  rw [forall_comm]
-  refine forall_congr' fun U ↦ ?_
-  simp_rw [HasAffineProperty.iff_of_isAffine, morphismRestrict_comp]
-  exact @H _ _ (f ∣_ U.1) U.2 (Scheme.OpenCover.restrict 𝒰 (f ⁻¹ᵁ U.1))
+  refine .mk_of_small (fun {X Y f} 𝒰 hf ↦ ?_) (fun {X Y f} 𝒰 hf ↦ ?_) <;>
+  simp_rw [IsZariskiLocalAtTarget.iff_of_iSup_eq_top _ (iSup_affineOpens_eq_top Y),
+      HasAffineProperty.iff_of_isAffine, morphismRestrict_comp] at hf ⊢
+  · intro i U
+    let 𝒰' : X.OpenCover := (Scheme.Cover.ulift 𝒰).add (𝒰.f i)
+    exact (H (f ∣_ U.1) (𝒰'.restrict _)).mp (hf _) none
+  · intro U
+    rw [H (f ∣_ U.1) (Scheme.OpenCover.restrict 𝒰 _)]
+    intro i
+    exact hf _ _
 
 end HasAffineProperty
 

Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean

@@ -225,7 +225,7 @@ theorem universally_isZariskiLocalAtTarget (P : MorphismProperty Scheme)
 
 lemma universally_isZariskiLocalAtSource (P : MorphismProperty Scheme)
     [IsZariskiLocalAtSource P] : IsZariskiLocalAtSource P.universally := by
-  refine .mk_of_iff ?_
+  refine .mk_of_iff_of_zeroHypercover ?_
   intro X Y f 𝒰
   refine ⟨fun hf i ↦ ?_, fun hf ↦ ?_⟩
   · apply MorphismProperty.universally_mk'

Mathlib/AlgebraicGeometry/Morphisms/LocalClosure.lean

@@ -73,12 +73,12 @@ instance [P.RespectsIso] : (sourceLocalClosure W P).RespectsIso where
 
 instance [P.RespectsIso] [P.RespectsLeft @IsOpenImmersion] :
     IsZariskiLocalAtSource (sourceLocalClosure IsOpenImmersion P) := by
-  refine .mk_of_iff fun f 𝒰 ↦ ?_
+  refine .mk_of_iff_of_zeroHypercover fun f 𝒰 ↦ ?_
   refine ⟨fun ⟨𝒱, h⟩ ↦ fun i ↦ ⟨𝒱.pullback₁ (𝒰.f i), fun j ↦ ?_⟩, fun h ↦ ?_⟩
   · simpa [pullback.condition_assoc] using
       RespectsLeft.precomp (Q := @IsOpenImmersion) _ inferInstance _ (h j)
   · choose 𝒱 h𝒱 using h
-    exact ⟨𝒰.bind 𝒱, fun i ↦ h𝒱 _ _⟩
+    exact ⟨(Scheme.Cover.ulift 𝒰).bind (fun i ↦ Scheme.Cover.ulift (𝒱 _)), fun i ↦ h𝒱 _ _⟩
 
 instance [P.IsStableUnderBaseChange] : (sourceLocalClosure W P).IsStableUnderBaseChange := by
   refine .mk' fun X Y S f g _ ⟨𝒰, hg⟩ ↦ ⟨𝒰.pullback₁ (pullback.snd f g), fun i ↦ ?_⟩

Mathlib/AlgebraicGeometry/Restrict.lean

@@ -854,7 +854,7 @@ set_option backward.isDefEq.respectTransparency false in
 /-- The restriction of an open cover to an open subset. -/
 @[simps! I₀ X f]
 noncomputable
-def Scheme.OpenCover.restrict {X : Scheme.{u}} (𝒰 : X.OpenCover) (U : Opens X) :
+def Scheme.OpenCover.restrict {X : Scheme.{u}} (𝒰 : Scheme.OpenCover.{v} X) (U : Opens X) :
     U.toScheme.OpenCover := by
   refine Cover.copy (𝒰.pullback₁ U.ι) 𝒰.I₀ _ (𝒰.f · ∣_ U) (Equiv.refl _)
     (fun i ↦ IsOpenImmersion.isoOfRangeEq (Opens.ι _) (pullback.snd _ _) ?_) ?_