AlgebraicGeometry.genericPoint_mem_preimage_comp_pullback_fst_of_injective_algebraMap
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace genericPoint_mem_preimage_comp_pullback_fst_of_injective_algebraMap
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.genericPoint_mem_preimage_comp_pullback_fst_of_injective_algebraMap
{R : Type u} [CommRing R] {K : Type u} [Field K] [Algebra R K]
(hinj : Function.Injective (algebraMap R K))
{X : Scheme.{u}} (c : X ⟶ Spec (.of R)) [IsIntegral X]
{Y : Scheme.{u}} [IsIntegral Y]
(e₀ : Y ⟶ pullback c (Spec.map (CommRingCat.ofHom (algebraMap R K)))) [IsIso e₀]
(U : X.Opens) (hU : (U : Set X).Nonempty) :
genericPoint Y ∈ (e₀ ≫ pullback.fst c (Spec.map (CommRingCat.ofHom (algebraMap R K)))) ⁻¹ᵁ U