Module

GeometricStalkFlat.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkFlat

4 declarations indexed from sourceView source ↗

Module documentation

Flatness of the actual geometric étale stalk

A finite family of germs and a relation among them descend to one pointed étale neighborhood. The filtered-colimit equality criterion makes that relation zero on a further neighborhood. Choose an actual affine open neighborhood of the geometric point there. Its structure map is étale, hence flat, so the relation is trivial by the equational criterion for flatness. Its witnesses map to witnesses in the geometric stalk.

This proves flatness of the structure map constructed in GeometricStalkStructure. It does not assume an affine-colimit presentation or flatness as a field of a strict-henselization package.

Imports8

Nyll.EtaleFundamentalGroups.StrictHenselian.GeometricStalkStructure
Mathlib.AlgebraicGeometry.AffineScheme
Mathlib.AlgebraicGeometry.Morphisms.Flat
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.RingTheory.Flat.EquationalCriterion
Mathlib.RingTheory.Flat.FaithfullyFlat.Algebra
Mathlib.RingTheory.RingHom.FaithfullyFlat
Mathlib.RingTheory.RingHom.Flat

Imported by23

theorem

geometricStalk_exists_affine_refinement

L42 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalk_exists_affine_refinement

Documentation

Every actual pointed étale neighborhood has an affine pointed étale refinement, constructed by lifting the geometric point to an affine open.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u

Lean source · statement

theorem geometricStalk_exists_affine_refinement
    {S : Scheme.{u}} {Ω : Type u} [Field Ω]
    (s : Spec (.of Ω) ⟶ S) (W : S.Etale)
    (t : (Scheme.pointEtaleNeighborhoods s).fiber.obj W) :
    ∃ (V : S.Etale) (v : (Scheme.pointEtaleNeighborhoods s).fiber.obj V) (f : V ⟶ W),
      IsAffine V.left ∧ (Scheme.pointEtaleNeighborhoods s).fiber.map f v = t

theorem

geometricStalkStructureMap_flat

L82 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_flat

Documentation

The actual structure map to the geometric étale stalk is flat. A finite relation is solved on an actual affine étale refinement and then mapped back.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω]
  (φ : R →+* Ω)

Lean source · statement

theorem geometricStalkStructureMap_flat : (geometricStalkStructureMap φ).Flat

theorem

geometricStalkStructureMap_faithfullyFlat

L167 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_faithfullyFlat

Documentation

At a closed geometric point of a local base, the constructed structure map is faithfully flat.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω]
  (φ : R →+* Ω)

Lean source · statement

theorem geometricStalkStructureMap_faithfullyFlat [IsLocalRing R] [IsLocalHom φ] :
    (geometricStalkStructureMap φ).FaithfullyFlat

theorem

geometricStalkStructureMap_injective

L180 ↗

EtaleFundamentalGroups.StrictHenselian.geometricStalkStructureMap_injective

Documentation

In particular, the local base ring embeds into its constructed geometric étale stalk.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleFundamentalGroups.StrictHenselian
universe u
variable {R Ω : Type u} [CommRing R] [Field Ω]
  (φ : R →+* Ω)

Lean source · statement

theorem geometricStalkStructureMap_injective [IsLocalRing R] [IsLocalHom φ] :
    Function.Injective (geometricStalkStructureMap φ)

Module documentation

Flatness of the actual geometric étale stalk

Declarations

geometricStalk_exists_affine_refinement

geometricStalkStructureMap_flat

geometricStalkStructureMap_faithfullyFlat

geometricStalkStructureMap_injective