refactor(AlgebraicGeometry): rename fields of Scheme.Cover to match ZeroHypercover (#29803)

This is in preparation for replacing `Scheme.Cover` by `ZeroHypercover` for the Zariski precoverage (see #29061). For consistency, also the fields of `Scheme.AffineCover` were updated accordingly.
Deprecations were added for the following renames:

- `Scheme.Cover.J` -> `Scheme.Cover.I₀`
- `Scheme.Cover.obj` -> `Scheme.Cover.X`
- `Scheme.Cover.map` -> `Scheme.Cover.f`

and similarly for `AffineCover`. No deprecations were added for the automatically generated `simps` lemmas, in the expectation that users will already get a deprecation warning for one of the fields above.

Author: chrisflav

Mathlib/AlgebraicGeometry/AffineScheme.lean

@@ -240,24 +240,24 @@ theorem exists_isAffineOpen_mem_and_subset {X : Scheme.{u}} {x : X}
   exact ⟨Scheme.Hom.opensRange f (H := hf.1),
     ⟨AlgebraicGeometry.isAffineOpen_opensRange f (H := hf.1), hf.2.1, hf.2.2⟩⟩
 
-instance Scheme.isAffine_affineCover (X : Scheme) (i : X.affineCover.J) :
-    IsAffine (X.affineCover.obj i) :=
+instance Scheme.isAffine_affineCover (X : Scheme) (i : X.affineCover.I₀) :
+    IsAffine (X.affineCover.X i) :=
   isAffine_Spec _
 
-instance Scheme.isAffine_affineBasisCover (X : Scheme) (i : X.affineBasisCover.J) :
-    IsAffine (X.affineBasisCover.obj i) :=
+instance Scheme.isAffine_affineBasisCover (X : Scheme) (i : X.affineBasisCover.I₀) :
+    IsAffine (X.affineBasisCover.X i) :=
   isAffine_Spec _
 
-instance Scheme.isAffine_affineOpenCover (X : Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.J) :
-    IsAffine (𝒰.openCover.obj i) :=
-  inferInstanceAs (IsAffine (Spec (𝒰.obj i)))
+instance Scheme.isAffine_affineOpenCover (X : Scheme) (𝒰 : X.AffineOpenCover) (i : 𝒰.I₀) :
+    IsAffine (𝒰.openCover.X i) :=
+  inferInstanceAs (IsAffine (Spec (𝒰.X i)))
 
-instance (X : Scheme) [CompactSpace X] (𝒰 : X.OpenCover) [∀ i, IsAffine (𝒰.obj i)] (i) :
-    IsAffine (𝒰.finiteSubcover.obj i) :=
-  inferInstanceAs (IsAffine (𝒰.obj _))
+instance (X : Scheme) [CompactSpace X] (𝒰 : X.OpenCover) [∀ i, IsAffine (𝒰.X i)] (i) :
+    IsAffine (𝒰.finiteSubcover.X i) :=
+  inferInstanceAs (IsAffine (𝒰.X _))
 
 instance {X} [IsAffine X] (i) :
-    IsAffine ((Scheme.coverOfIsIso (P := @IsOpenImmersion) (𝟙 X)).obj i) := by
+    IsAffine ((Scheme.coverOfIsIso (P := @IsOpenImmersion) (𝟙 X)).X i) := by
   dsimp; infer_instance
 
 theorem isBasis_affine_open (X : Scheme) : Opens.IsBasis X.affineOpens := by

Mathlib/AlgebraicGeometry/AffineSpace.lean

@@ -406,8 +406,8 @@ lemma isOpenMap_over : IsOpenMap (𝔸(n; S) ↘ S).base := by
   wlog hS : ∃ R, S = Spec R
   · refine (IsLocalAtTarget.iff_of_openCover (P := topologically @IsOpenMap) S.affineCover).mpr ?_
     intro i
-    have := this (n := n) (S.affineCover.obj i) ⟨_, rfl⟩
-    rwa [← (isPullback_map (n := n)  (S.affineCover.map i)).isoPullback_hom_snd,
+    have := this (n := n) (S.affineCover.X i) ⟨_, rfl⟩
+    rwa [← (isPullback_map (n := n)  (S.affineCover.f i)).isoPullback_hom_snd,
       MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)] at this
   obtain ⟨R, rfl⟩ := hS
   rw [← MorphismProperty.cancel_left_of_respectsIso (P := topologically @IsOpenMap)
@@ -434,8 +434,8 @@ lemma isIntegralHom_over_iff_isEmpty : IsIntegralHom (𝔸(n; S) ↘ S) ↔ IsEm
     wlog hS : ∃ R, S = Spec R
     · obtain ⟨x⟩ := ‹Nonempty S›
       obtain ⟨y, hy⟩ := S.affineCover.covers x
-      exact this (S.affineCover.obj x) (MorphismProperty.IsStableUnderBaseChange.of_isPullback
-        (isPullback_map (S.affineCover.map x)) h) ⟨y⟩ ⟨_, rfl⟩
+      exact this (S.affineCover.X x) (MorphismProperty.IsStableUnderBaseChange.of_isPullback
+        (isPullback_map (S.affineCover.f x)) h) ⟨y⟩ ⟨_, rfl⟩
     obtain ⟨R, rfl⟩ := hS
     have : Nontrivial R := (subsingleton_or_nontrivial R).resolve_left fun H ↦
         not_isEmpty_of_nonempty (Spec R) (inferInstanceAs (IsEmpty (PrimeSpectrum R)))

Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

@@ -43,17 +43,17 @@ lemma Scheme.nonempty_of_isLimit [IsCofilteredOrEmpty I]
   · have i := Nonempty.some ‹Nonempty I›
     have : IsCofiltered I := ⟨⟩
     let 𝒰 := (D.obj i).affineCover.finiteSubcover
-    have (i' : _) : IsAffine (𝒰.obj i') := inferInstanceAs (IsAffine (Spec _))
+    have (i' : _) : IsAffine (𝒰.X i') := inferInstanceAs (IsAffine (Spec _))
     obtain ⟨j, H⟩ :
-        ∃ j : 𝒰.J, ∀ {i'} (f : i' ⟶ i), Nonempty ((𝒰.pullbackCover (D.map f)).obj j) := by
+        ∃ j : 𝒰.I₀, ∀ {i'} (f : i' ⟶ i), Nonempty ((𝒰.pullbackCover (D.map f)).X j) := by
       simp_rw [← not_isEmpty_iff]
       by_contra! H
       choose i' f hf using H
       let g (j) := IsCofiltered.infTo (insert i (Finset.univ.image i'))
-        (Finset.univ.image fun j : 𝒰.J ↦ ⟨_, _, by simp, by simp, f j⟩) (X := j)
-      have (j : 𝒰.J) : IsEmpty ((𝒰.pullbackCover (D.map (g i (by simp)))).obj j) := by
-        let F : (𝒰.pullbackCover (D.map (g i (by simp)))).obj j ⟶
-            (𝒰.pullbackCover (D.map (f j))).obj j :=
+        (Finset.univ.image fun j : 𝒰.I₀ ↦ ⟨_, _, by simp, by simp, f j⟩) (X := j)
+      have (j : 𝒰.I₀) : IsEmpty ((𝒰.pullbackCover (D.map (g i (by simp)))).X j) := by
+        let F : (𝒰.pullbackCover (D.map (g i (by simp)))).X j ⟶
+            (𝒰.pullbackCover (D.map (f j))).X j :=
           pullback.map _ _ _ _ (D.map (g _ (by simp))) (𝟙 _) (𝟙 _) (by
             rw [← D.map_comp, IsCofiltered.infTo_commutes]
             · simp [g]
@@ -63,11 +63,11 @@ lemma Scheme.nonempty_of_isLimit [IsCofilteredOrEmpty I]
       obtain ⟨x, -⟩ :=
         (𝒰.pullbackCover (D.map (g i (by simp)))).covers (Nonempty.some inferInstance)
       exact (this _).elim x
-    let F := Over.post D ⋙ Over.pullback (𝒰.map j) ⋙ Over.forget _
+    let F := Over.post D ⋙ Over.pullback (𝒰.f j) ⋙ Over.forget _
     have (i' : _) : IsAffine (F.obj i') :=
-      have : IsAffineHom (pullback.snd (D.map i'.hom) (𝒰.map j)) :=
+      have : IsAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j)) :=
         MorphismProperty.pullback_snd _ _ inferInstance
-      isAffine_of_isAffineHom (pullback.snd (D.map i'.hom) (𝒰.map j))
+      isAffine_of_isAffineHom (pullback.snd (D.map i'.hom) (𝒰.f j))
     have (i' : _) : Nonempty (F.obj i') := H i'.hom
     let e : F ⟶ (F ⋙ Scheme.Γ.rightOp) ⋙ Scheme.Spec := Functor.whiskerLeft F ΓSpec.adjunction.unit
     have (i : _) : IsIso (e.app i) := IsAffine.affine
@@ -82,7 +82,7 @@ lemma Scheme.nonempty_of_isLimit [IsCofilteredOrEmpty I]
       exact CommRingCat.FilteredColimits.nontrivial
         (isColimitCoconeLeftOpOfCone _ (limit.isLimit (F ⋙ Scheme.Γ.rightOp)))
     let α : F ⟶ Over.forget _ ⋙ D := Functor.whiskerRight
-      (Functor.whiskerLeft (Over.post D) (Over.mapPullbackAdj (𝒰.map j)).counit) (Over.forget _)
+      (Functor.whiskerLeft (Over.post D) (Over.mapPullbackAdj (𝒰.f j)).counit) (Over.forget _)
     exact this.map (((Functor.Initial.isLimitWhiskerEquiv (Over.forget i) c).symm hc).lift
         ((Cones.postcompose α).obj c'.1)).base