AlgebraicGeometry.geometricallyIntegral_of_forall_isAlgClosed_isIntegral_pullback
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Curves.Proofs
namespace geometricallyIntegral_of_forall_isAlgClosed_isIntegral_pullback
open CategoryTheory CategoryTheory.Limits AlgebraicGeometryLean source · statement
theorem _root_.AlgebraicGeometry.geometricallyIntegral_of_forall_isAlgClosed_isIntegral_pullback
{R : Type} [CommRing R] {X : Scheme.{0}} (f : X ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType
f]
(hgeo : ∀ (k : Type) [Field k] [IsAlgClosed k] (s : Spec (CommRingCat.of k) ⟶ Spec
(CommRingCat.of R)),
AlgebraicGeometry.IsIntegral (pullback f s)) :
GeometricallyIntegral f