chore(AlgebraicGeometry): remove unnecessary uses of Hom.base (leanprover-community#30957)

The locations were found by a linter, that flagged every occurrence of the chain `DFunLike.coe`, `CategoryTheory.ConcreteCategory.hom` , `AlgebraicGeometry.PresheafedSpace.Hom.base`, `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` , `AlgebraicGeometry.Scheme.Hom.toLRSHom'` and an explicit `.base` projection.

Author: chrisflav

Mathlib/AlgebraicGeometry/AffineTransitionLimit.lean

@@ -43,7 +43,7 @@ lemma Scheme.nonempty_of_isLimit [IsCofilteredOrEmpty I]
   classical
   cases isEmpty_or_nonempty I
   · have e := (isLimitEquivIsTerminalOfIsEmpty _ _ hc).uniqueUpToIso specULiftZIsTerminal
-    exact Nonempty.map e.inv.base inferInstance
+    exact Nonempty.map e.inv inferInstance
   · have i := Nonempty.some ‹Nonempty I›
     have : IsCofiltered I := ⟨⟩
     let 𝒰 := (D.obj i).affineCover.finiteSubcover
@@ -62,7 +62,7 @@ lemma Scheme.nonempty_of_isLimit [IsCofilteredOrEmpty I]
             · simp [g]
             · simp
             · exact Finset.mem_image_of_mem _ (Finset.mem_univ _)) (by simp)
-        exact Function.isEmpty F.base
+        exact Function.isEmpty F
       obtain ⟨x, -⟩ :=
         Cover.covers (𝒰.pullback₁ (D.map (g i (by simp)))) (Nonempty.some inferInstance)
       exact (this _).elim x
@@ -87,7 +87,7 @@ lemma Scheme.nonempty_of_isLimit [IsCofilteredOrEmpty I]
     let α : F ⟶ Over.forget _ ⋙ D := Functor.whiskerRight
       (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
+        ((Cones.postcompose α).obj c'.1))
 
 include hc in
 open Scheme.IdealSheafData in
@@ -102,8 +102,8 @@ lemma exists_mem_of_isClosed_of_nonempty
     (hZc : ∀ (i : I), IsClosed (Z i))
     (hZne : ∀ i, (Z i).Nonempty)
     (hZcpt : ∀ i, IsCompact (Z i))
-    (hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (D.map f).base (Z i) (Z i')) :
-    ∃ (s : c.pt), ∀ i, (c.π.app i).base s ∈ Z i := by
+    (hmapsTo : ∀ {i i' : I} (f : i ⟶ i'), Set.MapsTo (D.map f) (Z i) (Z i')) :
+    ∃ (s : c.pt), ∀ i, c.π.app i s ∈ Z i := by
   let D' : I ⥤ Scheme :=
   { obj i := (vanishingIdeal ⟨Z i, hZc i⟩).subscheme
     map {X Y} f := subschemeMap _ _ (D.map f) (by
@@ -153,8 +153,8 @@ lemma exists_mem_of_isClosed_of_nonempty'
     (hZne : ∀ i hij, (Z i hij).Nonempty)
     (hZcpt : ∀ i hij, IsCompact (Z i hij))
     (hstab : ∀ (i i' : I) (hi'i : i' ⟶ i) (hij : i ⟶ j),
-      Set.MapsTo (D.map hi'i).base (Z i' (hi'i ≫ hij)) (Z i hij)) :
-    ∃ (s : c.pt), ∀ i hij, (c.π.app i).base s ∈ Z i hij := by
+      Set.MapsTo (D.map hi'i) (Z i' (hi'i ≫ hij)) (Z i hij)) :
+    ∃ (s : c.pt), ∀ i hij, c.π.app i s ∈ Z i hij := by
   have {i₁ i₂ : Over j} (f : i₁ ⟶ i₂) : IsAffineHom ((Over.forget j ⋙ D).map f) := by
     dsimp; infer_instance
   simpa [Over.forall_iff] using exists_mem_of_isClosed_of_nonempty (Over.forget j ⋙ D) _
@@ -383,19 +383,19 @@ variable (A : ExistsHomHomCompEqCompAux D t f)
 
 omit [LocallyOfFiniteType f] in
 lemma exists_index : ∃ (i' : I) (hii' : i' ⟶ A.i),
-    ((D.map hii' ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb)).base ⁻¹'
+    ((D.map hii' ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb)) ⁻¹'
       ((Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X : Set <|
         ↑(pullback f f))ᶜ)) = ∅ := by
   let W := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
   by_contra! h
   let Z (i' : I) (hii' : i' ⟶ A.i) :=
-    (D.map hii' ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb)).base ⁻¹' Wᶜ
+    (D.map hii' ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb)) ⁻¹' Wᶜ
   have hZ (i') (hii' : i' ⟶ A.i) : IsClosed (Z i' hii') :=
     (W.isOpen.isClosed_compl).preimage <| Scheme.Hom.continuous _
   obtain ⟨s, hs⟩ := exists_mem_of_isClosed_of_nonempty' D A.c A.hc Z hZ h
     (fun _ _ ↦ (hZ _ _).isCompact) (fun i i' hii' hij ↦ by simp [Z, Set.MapsTo])
   refine hs A.i (𝟙 A.i) (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ?_)
-  use (A.c.π.app A.i ≫ A.a).base s
+  use (A.c.π.app A.i ≫ A.a) s
   have H : A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f =
       A.c.π.app A.i ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb) := by ext <;> simp [hab]
   simp [← Scheme.Hom.comp_apply, - Scheme.Hom.comp_base, H]
@@ -416,7 +416,7 @@ def g : D.obj A.i' ⟶ pullback f f :=
 
 omit [LocallyOfFiniteType f] in
 lemma range_g_subset :
-    Set.range A.g.base ⊆ Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X := by
+    Set.range A.g ⊆ Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X := by
   simpa [ExistsHomHomCompEqCompAux.hii', g] using A.exists_index.choose_spec.choose_spec
 
 /-- (Implementation)

Mathlib/AlgebraicGeometry/Cover/Directed.lean

@@ -45,7 +45,7 @@ class LocallyDirected (𝒰 : X.Cover (precoverage P)) [Category 𝒰.I₀] wher
   w {i j : 𝒰.I₀} (hij : i ⟶ j) : trans hij ≫ 𝒰.f j = 𝒰.f i := by aesop_cat
   directed {i j : 𝒰.I₀} (x : (pullback (𝒰.f i) (𝒰.f j)).carrier) :
     ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : 𝒰.X k),
-      (pullback.lift (trans hki) (trans hkj) (by simp [w])).base y = x
+      pullback.lift (trans hki) (trans hkj) (by simp [w]) y = x
   property_trans {i j : 𝒰.I₀} (hij : i ⟶ j) : P (trans hij) := by infer_instance
 
 variable (𝒰 : X.Cover (precoverage P)) [Category 𝒰.I₀] [𝒰.LocallyDirected]
@@ -66,7 +66,7 @@ lemma trans_comp {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k) :
 
 lemma exists_lift_trans_eq {i j : 𝒰.I₀} (x : (pullback (𝒰.f i) (𝒰.f j)).carrier) :
     ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : 𝒰.X k),
-      (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) (by simp)).base y = x :=
+      pullback.lift (𝒰.trans hki) (𝒰.trans hkj) (by simp) y = x :=
   LocallyDirected.directed x
 
 lemma property_trans {i j : 𝒰.I₀} (hij : i ⟶ j) : P (𝒰.trans hij) :=
@@ -100,7 +100,7 @@ instance : (𝒰.functorOfLocallyDirected ⋙ Scheme.forget).IsLocallyDirected w
   cond {i j k} fi fj xi xj hxij := by
     simp only [Functor.comp_obj, Cover.functorOfLocallyDirected_obj, forget_obj, Functor.comp_map,
       Cover.functorOfLocallyDirected_map, forget_map] at hxij
-    have : (𝒰.f i).base xi = (𝒰.f j).base xj := by
+    have : 𝒰.f i xi = 𝒰.f j xj := by
       rw [← 𝒰.trans_map fi, ← 𝒰.trans_map fj, Hom.comp_base, Hom.comp_base,
         ConcreteCategory.comp_apply, hxij, ConcreteCategory.comp_apply]
     obtain ⟨z, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback xi xj this
@@ -142,10 +142,10 @@ instance locallyDirectedPullbackCover : Cover.LocallyDirected (𝒰.pullback₁
           pullback.map _ _ _ _ (𝟙 Y) (pullback.lift (𝒰.trans hki) (𝒰.trans hkj) (by simp)) (𝟙 X)
             (by simp) (by simp) ≫ iso.inv := by
       apply pullback.hom_ext <;> apply pullback.hom_ext <;> simp [iso]
-    obtain ⟨k, hki, hkj, yk, hyk⟩ := 𝒰.exists_lift_trans_eq ((iso.hom ≫ pullback.snd _ _).base x)
+    obtain ⟨k, hki, hkj, yk, hyk⟩ := 𝒰.exists_lift_trans_eq ((iso.hom ≫ pullback.snd _ _) x)
     refine ⟨k, hki, hkj, show x ∈ Set.range _ from ?_⟩
     rw [this, Scheme.Hom.comp_base, TopCat.coe_comp, Set.range_comp, Pullback.range_map]
-    use iso.hom.base x
+    use iso.hom x
     simp only [Hom.id_base, TopCat.hom_id, ContinuousMap.coe_id, Set.range_id, Set.preimage_univ,
       Set.univ_inter, Set.mem_preimage, Set.mem_range, hom_inv_apply, and_true]
     exact ⟨yk, hyk⟩
@@ -232,7 +232,7 @@ def Cover.LocallyDirected.ofIsBasisOpensRange {𝒰 : X.OpenCover} [Preorder 
   trans_id i := by rw [← cancel_mono (𝒰.f i)]; simp
   trans_comp hij hjk := by rw [← cancel_mono (𝒰.f _)]; simp
   directed {i j} x := by
-    have : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).base x ∈
+    have : (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i) x ∈
       (pullback.fst (𝒰.f i) (𝒰.f j) ≫ 𝒰.f i).opensRange := ⟨x, rfl⟩
     obtain ⟨k, ⟨k, rfl⟩, ⟨y, hy⟩, h⟩ := TopologicalSpace.Opens.isBasis_iff_nbhd.mp H this
     refine ⟨k, homOfLE <| hle.mpr <| le_trans h ?_, homOfLE <| hle.mpr <| le_trans h ?_, y, ?_⟩

Mathlib/AlgebraicGeometry/Cover/MorphismProperty.lean

@@ -40,7 +40,7 @@ variable (K : Precoverage Scheme.{u})
 is jointly surjective. -/
 class JointlySurjective (K : Precoverage Scheme.{u}) : Prop where
   exists_eq {X : Scheme.{u}} (S : Presieve X) (hS : S ∈ K X) (x : X) :
-    ∃ (Y : Scheme.{u}) (g : Y ⟶ X), S g ∧ x ∈ Set.range g.base
+    ∃ (Y : Scheme.{u}) (g : Y ⟶ X), S g ∧ x ∈ Set.range g
 
 /-- A cover of `X` in the coverage `K` is a `0`-hypercover for `K`. -/
 abbrev Cover (K : Precoverage Scheme.{u}) := Precoverage.ZeroHypercover.{v} K
@@ -51,7 +51,7 @@ variable {X Y Z : Scheme.{u}} (𝒰 : X.Cover K) (f : X ⟶ Z) (g : Y ⟶ Z)
 variable [∀ x, HasPullback (𝒰.f x ≫ f) g]
 
 lemma Cover.exists_eq [JointlySurjective K] (𝒰 : X.Cover K) (x : X) :
-    ∃ i y, (𝒰.f i).base y = x := by
+    ∃ i y, 𝒰.f i y = x := by
   obtain ⟨Y, g, ⟨i⟩, y, hy⟩ := JointlySurjective.exists_eq 𝒰.presieve₀ 𝒰.mem₀ x
   use i, y
 
@@ -60,11 +60,11 @@ def Cover.idx [JointlySurjective K] (𝒰 : X.Cover K) (x : X) : 𝒰.I₀ :=
   (𝒰.exists_eq x).choose
 
 lemma Cover.covers [JointlySurjective K] (𝒰 : X.Cover K) (x : X) :
-    x ∈ Set.range (𝒰.f (𝒰.idx x)).base :=
+    x ∈ Set.range (𝒰.f (𝒰.idx x)) :=
   (𝒰.exists_eq x).choose_spec
 
 theorem Cover.iUnion_range [JointlySurjective K] {X : Scheme.{u}} (𝒰 : X.Cover K) :
-    ⋃ i, Set.range (𝒰.f i).base = Set.univ := by
+    ⋃ i, Set.range (𝒰.f i) = Set.univ := by
   rw [Set.eq_univ_iff_forall]
   intro x
   rw [Set.mem_iUnion]
@@ -80,7 +80,7 @@ section MorphismProperty
 variable {P Q : MorphismProperty Scheme.{u}}
 
 lemma presieve₀_mem_precoverage_iff (E : PreZeroHypercover X) :
-    E.presieve₀ ∈ precoverage P X ↔ (∀ x, ∃ i, x ∈ Set.range (E.f i).base) ∧ ∀ i, P (E.f i) := by
+    E.presieve₀ ∈ precoverage P X ↔ (∀ x, ∃ i, x ∈ Set.range (E.f i)) ∧ ∀ i, P (E.f i) := by
   simp
 
 @[grind ←]
@@ -91,7 +91,7 @@ lemma Cover.map_prop (𝒰 : X.Cover (precoverage P)) (i : 𝒰.I₀) : P (𝒰.
 cover `X`, `Cover.mkOfCovers` is an associated `P`-cover of `X`. -/
 @[simps!]
 def Cover.mkOfCovers (J : Type*) (obj : J → Scheme.{u}) (map : (j : J) → obj j ⟶ X)
-    (covers : ∀ x, ∃ j y, (map j).base y = x)
+    (covers : ∀ x, ∃ j y, map j y = x)
     (map_prop : ∀ j, P (map j) := by infer_instance) : X.Cover (precoverage P) where
   I₀ := J
   X := obj
@@ -106,7 +106,7 @@ def coverOfIsIso [P.ContainsIdentities] [P.RespectsIso] {X Y : Scheme.{u}} (f :
     [IsIso f] : Cover.{v} (precoverage P) Y :=
   .mkOfCovers PUnit (fun _ ↦ X)
     (fun _ ↦ f)
-    (fun x ↦ ⟨⟨⟩, (inv f).base x, by simp [← Hom.comp_apply]⟩)
+    (fun x ↦ ⟨⟨⟩, inv f x, by simp [← Hom.comp_apply]⟩)
     (fun _ ↦ P.of_isIso f)
 
 instance : JointlySurjective (precoverage P) where
@@ -141,7 +141,7 @@ def Cover.copy [P.RespectsIso] {X : Scheme.{u}} (𝒰 : X.Cover (precoverage P))
     refine ⟨fun x ↦ ?_, ?_⟩
     · obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq x
       obtain ⟨i, rfl⟩ := e₁.surjective i
-      use i, (e₂ i).inv.base y
+      use i, (e₂ i).inv y
       simp [h]
     · simp_rw [h, MorphismProperty.cancel_left_of_respectsIso]
       intro i
@@ -201,7 +201,7 @@ structure AffineCover (P : MorphismProperty Scheme.{u}) (S : Scheme.{u}) where
   /-- given a point of `x : S`, `idx x` is the index of the component which contains `x` -/
   idx (x : S) : I₀
   /-- the components cover `S` -/
-  covers (x : S) : x ∈ Set.range (f (idx x)).base
+  covers (x : S) : x ∈ Set.range (f (idx x))
   /-- the component maps satisfy `P` -/
   map_prop (j : I₀) : P (f j) := by infer_instance
 

Mathlib/AlgebraicGeometry/Cover/Open.lean

@@ -77,10 +77,10 @@ lemma OpenCover.isOpenCover_opensRange {X : Scheme.{u}} (𝒰 : X.OpenCover) :
 def OpenCover.finiteSubcover {X : Scheme.{u}} (𝒰 : OpenCover X) [H : CompactSpace X] :
     OpenCover X := by
   have :=
-    @CompactSpace.elim_nhds_subcover _ _ H (fun x : X => Set.range (𝒰.f (𝒰.idx x)).base)
+    @CompactSpace.elim_nhds_subcover _ _ H (fun x : X => Set.range (𝒰.f (𝒰.idx x)))
       fun x => (IsOpenImmersion.isOpen_range (𝒰.f (𝒰.idx x))).mem_nhds (𝒰.covers x)
   let t := this.choose
-  have h : ∀ x : X, ∃ y : t, x ∈ Set.range (𝒰.f (𝒰.idx y)).base := by
+  have h : ∀ x : X, ∃ y : t, x ∈ Set.range (𝒰.f (𝒰.idx y)) := by
     intro x
     have h' : x ∈ (⊤ : Set X) := trivial
     rw [← Classical.choose_spec this, Set.mem_iUnion] at h'
@@ -283,8 +283,8 @@ theorem affineBasisCover_obj (X : Scheme.{u}) (i : X.affineBasisCover.I₀) :
 
 theorem affineBasisCover_map_range (X : Scheme.{u}) (x : X)
     (r : (X.local_affine x).choose_spec.choose) :
-    Set.range (X.affineBasisCover.f ⟨x, r⟩).base =
-      (X.affineCover.f x).base '' (PrimeSpectrum.basicOpen r).1 := by
+    Set.range (X.affineBasisCover.f ⟨x, r⟩) =
+      (X.affineCover.f x) '' (PrimeSpectrum.basicOpen r).1 := by
   simp only [affineBasisCover, Precoverage.ZeroHypercover.bind_toPreZeroHypercover, Set.range_comp,
     PreZeroHypercover.bind_f, Hom.comp_base, TopCat.hom_comp, ContinuousMap.coe_comp]
   congr
@@ -293,16 +293,16 @@ theorem affineBasisCover_map_range (X : Scheme.{u}) (x : X)
 theorem affineBasisCover_is_basis (X : Scheme.{u}) :
     TopologicalSpace.IsTopologicalBasis
       {x : Set X |
-        ∃ a : X.affineBasisCover.I₀, x = Set.range (X.affineBasisCover.f a).base} := by
+        ∃ a : X.affineBasisCover.I₀, x = Set.range (X.affineBasisCover.f a)} := by
   apply TopologicalSpace.isTopologicalBasis_of_isOpen_of_nhds
   · rintro _ ⟨a, rfl⟩
     exact IsOpenImmersion.isOpen_range (X.affineBasisCover.f a)
   · rintro a U haU hU
     rcases X.affineCover.covers a with ⟨x, e⟩
-    let U' := (X.affineCover.f (X.affineCover.idx a)).base ⁻¹' U
+    let U' := (X.affineCover.f (X.affineCover.idx a)) ⁻¹' U
     have hxU' : x ∈ U' := by rw [← e] at haU; exact haU
     rcases PrimeSpectrum.isBasis_basic_opens.exists_subset_of_mem_open hxU'
-        ((X.affineCover.f (X.affineCover.idx a)).base.hom.continuous_toFun.isOpen_preimage _
+        ((X.affineCover.f (X.affineCover.idx a)).continuous.isOpen_preimage _
           hU) with
       ⟨_, ⟨_, ⟨s, rfl⟩, rfl⟩, hxV, hVU⟩
     refine ⟨_, ⟨⟨_, s⟩, rfl⟩, ?_, ?_⟩ <;> rw [affineBasisCover_map_range]

Mathlib/AlgebraicGeometry/Cover/Sigma.lean

@@ -31,7 +31,7 @@ noncomputable def sigma (𝒰 : Cover.{v} (precoverage P) S) : S.Cover (precover
     rw [presieve₀_mem_precoverage_iff]
     refine ⟨fun s ↦ ?_, fun _ ↦ IsZariskiLocalAtSource.sigmaDesc 𝒰.map_prop⟩
     obtain ⟨i, y, rfl⟩ := 𝒰.exists_eq s
-    refine ⟨default, (Sigma.ι 𝒰.X i).base y, by simp [← Scheme.Hom.comp_apply]⟩
+    refine ⟨default, Sigma.ι 𝒰.X i y, by simp [← Scheme.Hom.comp_apply]⟩
 
 variable [P.IsMultiplicative] {𝒰 𝒱 : Scheme.Cover.{v} (precoverage P) S}