AlgebraicGeometry.SmoothProperCurve.exists_finite_etale_isClosedImmersion_le_finrank_of_finiteMapData
Etale level sets of finite maps give finite etale closed subschemes of arbitrarily large rank after a finite faithfully flat etale extension of a local noetherian base.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.SmoothProperCurve
universe u
open _root_.AlgebraicCurves.Geometry.Curves.Proofs in
open SmoothProperCurve_exists_finite_etale_isClosedImmersion_le_finrank_of_finiteMapData in
open scoped TensorProduct in
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.SmoothProperCurve in
open NeronModelInfra inLean source · statement
theorem exists_finite_etale_isClosedImmersion_le_finrank_of_finiteMapData
(R : Type u) [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
{C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
[SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(h𝔉 : ∀ m₀ : ℕ, ∃ 𝔉 : SmoothProperCurve.FiniteMapData c ε, m₀ ≤ 𝔉.m ∧
𝔉.LevelSetsGenericallyEtale) (N : ℕ) :
∃ (R₀ : Type u) (_ : CommRing R₀) (_ : Algebra R R₀) (_ : Module.Finite R R₀)
(_ : Algebra.Etale R R₀) (_ : Module.FaithfullyFlat R R₀) (_ : IsLocalRing R₀) (_ :
IsNoetherianRing R₀)
(B : Type u) (_ : CommRing B) (_ : Algebra R₀ B) (_ : Module.Finite R₀ B) (_ : Algebra.Etale
R₀ B)
(ι : Spec (CommRingCat.of B) ⟶ pullback c (specMap R R₀)),
IsClosedImmersion ι ∧ ι ≫ baseChange R c R₀ = specMap R₀ B ∧ N ≤ Module.finrank R₀ B