Module

FiniteRadicialLocalSplitting.lean

Nyll.SchemeTheory.Etale.FiniteRadicialLocalSplitting

2 declarations indexed from sourceView source ↗

Module documentation

Actual local sections of affine étale schemes over a finite radicial base

First choose an étale extension of the bottom ring that removes the separable part of the selected residue extension. The quasi-finite structure theorem then constructs a finite open factor with singleton fiber. Its actual map to the base change of the radicial scheme is finite and étale. The isomorphism neighborhood gives a section, and restricting the bottom étale neighborhood gives the asserted lift of the original cover.

No flatness or finite-presentation hypothesis is imposed on the finite radicial map. A chosen point of the cover suffices; surjectivity of the radicial map is not needed for this pointwise local statement.

Imports9

Nyll.SchemeTheory.Etale.ChosenResidueExtension
Nyll.SchemeTheory.Etale.PurelyInseparableFiniteFactor
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Morphisms.Finite
Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.Restrict
Mathlib.RingTheory.RingHom.Etale
Mathlib.RingTheory.Unramified.LocalStructure

Imported by2

theorem

etale_specMap_includeRight

L43 ↗

AlgebraicGeometry.etale_specMap_includeRight

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public noncomputable section
open CategoryTheory Limits
open scoped TensorProduct
universe u
namespace AlgebraicGeometry

Lean source · statement

theorem etale_specMap_includeRight
    (R T A : Type u) [CommRing R] [CommRing T] [CommRing A]
    [Algebra R T] [Algebra R A] [Algebra.Etale R T] :
    Etale (Spec.map (CommRingCat.ofHom
      (Algebra.TensorProduct.includeRight : A →ₐ[R] T ⊗[R] A).toRingHom))

theorem

exists_local_section_of_finite_radicial

L61 ↗

AlgebraicGeometry.Etale.exists_local_section_of_finite_radicial

Documentation

Through every point of an affine étale scheme upstairs, a finite radicial morphism admits an actual étale neighborhood downstairs on whose base change the cover has a section. The lift, its equation over the original base, and a point mapping to the prescribed point of the cover are all constructed.