AlgebraicGeometry.smooth_isProper_geometricallyConnected_of_faithfullyFlat_baseChange
Smoothness, properness and geometric connectedness descend along any faithfully flat change of affine base.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
universe u
open CategoryTheory CategoryTheory.Limits
open AlgebraicCurves.Geometry.Curves.Proofs
open smooth_isProper_geometricallyConnected_of_finiteEtale_baseChange.AlgebraicGeometry
open FiniteEtaleBaseChangeDescent
namespace AlgebraicGeometryLean source · statement
theorem smooth_isProper_geometricallyConnected_of_faithfullyFlat_baseChange
(R : Type u) [CommRing R] (R' : Type u) [CommRing R'] [Algebra R R']
[Module.FaithfullyFlat R R']
{X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of R)) {X' : Scheme.{u}} (x' : X' ⟶ Spec
(CommRingCat.of R'))
(hsm : Smooth x') (hpr : IsProper x') (hgc : GeometricallyConnected x')
(e : pullback f (Spec.map (CommRingCat.ofHom (algebraMap R R'))) ≅ X')
(he : e.hom ≫ x' = pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R R')))) :
Smooth f ∧ IsProper f ∧ GeometricallyConnected f