feat(Stalks): add exists_le_germ_eq (#39490)

Also rename `germ_exist` to `exists_germ_eq` to follow the naming convention.

Motivated by the Cauchy theorem project at ICERM workshop
"Techniques and Tools for the Formalization of Analysis".

Author: urkud

Mathlib/AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean

@@ -313,7 +313,7 @@ def homogeneousLocalizationToStalk (x : ProjectiveSpectrum.top 𝒜) (y : at x)
 
 lemma homogeneousLocalizationToStalk_stalkToFiberRingHom (x z) :
     homogeneousLocalizationToStalk 𝒜 x (stalkToFiberRingHom 𝒜 x z) = z := by
-  obtain ⟨U, hxU, s, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.germ_exist x z
+  obtain ⟨U, hxU, s, rfl⟩ := (Proj.structureSheaf 𝒜).presheaf.exists_germ_eq z
   change homogeneousLocalizationToStalk 𝒜 x ((stalkToFiberRingHom 𝒜 x).hom
       (((Proj.structureSheaf 𝒜).presheaf.germ U x hxU) s)) =
     ((Proj.structureSheaf 𝒜).presheaf.germ U x hxU) s

Mathlib/AlgebraicGeometry/Properties.lean

@@ -85,7 +85,7 @@ instance isReduced_stalk_of_isReduced [IsReduced X] (x : X) :
     _root_.IsReduced (X.presheaf.stalk x) := by
   constructor
   rintro g ⟨n, e⟩
-  obtain ⟨U, hxU, s, (rfl : (X.presheaf.germ U x hxU) s = g)⟩ := X.presheaf.germ_exist x g
+  obtain ⟨U, hxU, s, (rfl : (X.presheaf.germ U x hxU) s = g)⟩ := X.presheaf.exists_germ_eq g
   rw [← map_pow, ← map_zero (X.presheaf.germ _ x hxU).hom] at e
   obtain ⟨V, hxV, iU, iV, (e' : (X.presheaf.map iU.op) (s ^ n) = (X.presheaf.map iV.op) 0)⟩ :=
     X.presheaf.germ_eq x hxU hxU _ 0 e

Mathlib/AlgebraicGeometry/Spec.lean

@@ -356,7 +356,7 @@ def toPushforwardStalkAlgHom :
 
 theorem isLocalizedModule_toPushforwardStalkAlgHom_aux (y) :
     ∃ x : S × p.asIdeal.primeCompl, x.2 • y = toPushforwardStalkAlgHom R S p x.1 := by
-  obtain ⟨U, hp, s, e⟩ := TopCat.Presheaf.germ_exist _ _ y
+  obtain ⟨U, hp, s, e⟩ := TopCat.Presheaf.exists_germ_eq _ y
   obtain ⟨_, ⟨r, rfl⟩, hpr : p ∈ PrimeSpectrum.basicOpen r, hrU : PrimeSpectrum.basicOpen r ≤ U⟩ :=
     PrimeSpectrum.isTopologicalBasis_basic_opens.exists_subset_of_mem_open (show p ∈ U from hp) U.2
   change PrimeSpectrum.basicOpen r ≤ U at hrU

Mathlib/AlgebraicGeometry/SpreadingOut.lean

@@ -245,7 +245,7 @@ lemma exists_lift_of_germInjective_aux {U : X.Opens} {x : X} (hxU)
       V ≤ U ∧ RingHom.range φ.hom ≤ RingHom.range (X.presheaf.germ V x hxV).hom := by
   letI := φRA.hom.toAlgebra
   obtain ⟨s, hs⟩ := hφRA
-  choose W hxW f hf using fun t ↦ X.presheaf.germ_exist x (φ t)
+  choose W hxW f hf using fun t ↦ X.presheaf.exists_germ_eq (φ t)
   have H : x ∈ s.inf W ⊓ U := by
     rw [← SetLike.mem_coe, TopologicalSpace.Opens.coe_inf, TopologicalSpace.Opens.coe_finset_inf]
     exact ⟨by simpa using fun x _ ↦ hxW x, hxU⟩

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -600,7 +600,7 @@ def modulePresheafStalkIso (x : PrimeSpectrum.Top R) :
       Limits.colimit.isoColimitCocone ⟨_, Limits.isColimitOfPreserves (forget₂ (ModuleCat R) Ab)
       (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙
         structurePresheafInModuleCat R M))⟩
-    obtain ⟨U, hxU, s, rfl⟩ := TopCat.Presheaf.germ_exist _ _ m
+    obtain ⟨U, hxU, s, rfl⟩ := TopCat.Presheaf.exists_germ_eq _ m
     have : TopCat.Presheaf.germ (moduleStructurePresheaf R M).presheaf U x hxU ≫ α.hom =
         (forget₂ _ _).map ((structurePresheafInModuleCat R M).germ U x hxU) :=
       Limits.colimit.isoColimitCocone_ι_hom (C := Ab) ..
@@ -828,7 +828,7 @@ def commRingCatStalkEquivModuleStalk (x : PrimeSpectrum.Top R) :
       (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
       (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙
         structurePresheafInCommRingCat R))⟩)
-    obtain ⟨U, hxU, s, rfl⟩ := TopCat.Presheaf.germ_exist _ _ m
+    obtain ⟨U, hxU, s, rfl⟩ := TopCat.Presheaf.exists_germ_eq _ m
     have : (TopCat.Presheaf.germ (moduleStructurePresheaf R R).presheaf U x hxU) ≫ α.hom =
         (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map
           ((structurePresheafInCommRingCat R).germ U x hxU) :=

Mathlib/Geometry/Manifold/Sheaf/LocallyRingedSpace.lean

@@ -64,7 +64,7 @@ theorem smoothSheafCommRing.isUnit_stalk_iff {x : M}
     rintro (hf : _ ≠ 0)
     -- Represent `f` as the germ of some function (also called `f`) on an open neighbourhood `U` of
     -- `x`, which is nonzero at `x`
-    obtain ⟨U : Opens M, hxU, f : C^∞⟮IM, U; 𝓘(𝕜), 𝕜⟯, rfl⟩ := S.germ_exist x f
+    obtain ⟨U : Opens M, hxU, f : C^∞⟮IM, U; 𝓘(𝕜), 𝕜⟯, rfl⟩ := S.exists_germ_eq f
     have hf' : f ⟨x, hxU⟩ ≠ 0 := by
       convert hf
       exact (smoothSheafCommRing.eval_germ U x hxU f).symm

Mathlib/Geometry/RingedSpace/Basic.lean

@@ -76,7 +76,7 @@ theorem isUnit_res_of_isUnit_germ (U : Opens X) (f : X.presheaf.obj (op U)) (x :
     (h : IsUnit (X.presheaf.germ U x hx f)) :
     ∃ (V : Opens X) (i : V ⟶ U) (_ : x ∈ V), IsUnit (X.presheaf.map i.op f) := by
   obtain ⟨g', heq⟩ := h.exists_right_inv
-  obtain ⟨V, hxV, g, rfl⟩ := X.presheaf.germ_exist x g'
+  obtain ⟨V, hxV, g, rfl⟩ := X.presheaf.exists_germ_eq g'
   let W := U ⊓ V
   have hxW : x ∈ W := ⟨hx, hxV⟩
   replace heq : (X.presheaf.germ _ x hxW) ((X.presheaf.map (U.infLELeft V).op) f *

Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean

@@ -223,7 +223,7 @@ theorem coequalizer_π_stalk_isLocalHom (x : Y) :
     IsLocalHom ((coequalizer.π f.toShHom g.toShHom :).hom.stalkMap x).hom := by
   constructor
   rintro a ha
-  rcases TopCat.Presheaf.germ_exist _ _ a with ⟨U, hU, s, rfl⟩
+  rcases TopCat.Presheaf.exists_germ_eq _ a with ⟨U, hU, s, rfl⟩
   rw [PresheafedSpace.stalkMap_germ_apply (coequalizer.π f.toShHom g.toShHom).hom U _ hU] at ha
   let V := imageBasicOpen f g U s
   have hV : (coequalizer.π f.toShHom g.toShHom).hom.base ⁻¹'

Mathlib/Topology/Sheaves/LocallySurjective.lean

@@ -88,7 +88,7 @@ theorem locally_surjective_iff_surjective_on_stalks (T : ℱ ⟶ 𝒢) :
     -- Let g ∈ Γₛₜ 𝒢 x be a germ.
     intro x g
     -- Represent it on an open set U ⊆ X as ⟨t, U⟩.
-    obtain ⟨U, hxU, t, rfl⟩ := 𝒢.germ_exist x g
+    obtain ⟨U, hxU, t, rfl⟩ := 𝒢.exists_germ_eq g
     -- By local surjectivity, pass to a smaller open set V
     -- on which there exists s ∈ Γ_ ℱ V mapping to t |_ V.
     rcases hT.imageSieve_mem t x hxU with ⟨V, ι, ⟨s, h_eq⟩, hxV⟩
@@ -105,7 +105,7 @@ theorem locally_surjective_iff_surjective_on_stalks (T : ℱ ⟶ 𝒢) :
     intro U t x hxU
     set t_x := 𝒢.germ _ x hxU t with ht_x
     obtain ⟨s_x, hs_x : ((stalkFunctor C x).map T) s_x = t_x⟩ := hT x t_x
-    obtain ⟨V, hxV, s, rfl⟩ := ℱ.germ_exist x s_x
+    obtain ⟨V, hxV, s, rfl⟩ := ℱ.exists_germ_eq s_x
     -- rfl : ℱ.germ x s = s_x
     have key_W := 𝒢.germ_eq x hxV hxU (T.app _ s) t <| by
       convert hs_x using 1

Mathlib/Topology/Sheaves/Sheafify.lean

@@ -90,7 +90,7 @@ def stalkToFiber (x : X) : F.sheafify.presheaf.stalk x ⟶ F.stalk x :=
 theorem stalkToFiber_surjective (x : X) : Function.Surjective (F.stalkToFiber x) := by
   apply TopCat.stalkToFiber_surjective
   intro t
-  obtain ⟨U, m, s, rfl⟩ := F.germ_exist _ t
+  obtain ⟨U, m, s, rfl⟩ := F.exists_germ_eq t
   use ⟨U, m⟩
   fconstructor
   · exact fun y => F.germ _ _ y.2 s