Module

FieldSourceNormalization.lean

Nyll.EtaleFundamentalGroups.Normalization.FieldSourceNormalization

2 declarations indexed from sourceView source ↗

Module documentation

Normalization at a supplied generic field source

If the actual generic fiber of a finite étale morphism is a field spectrum, its source is connected. Over a normal integral base it is therefore the normalization in its function field. The generic pullback identifies that function-field spectrum with the given field spectrum, transporting the normalization isomorphism and its étaleness to the given extension.

Imports10

Nyll.EtaleFundamentalGroups.Normalization.GenericFieldSource
Nyll.EtaleFundamentalGroups.Inertia.NormalizationSourceIso
Nyll.EtaleFundamentalGroups.FiniteEtale.Connected
Nyll.EtaleFundamentalGroups.FiniteEtale.Integral
Nyll.EtaleFundamentalGroups.Purity.PuncturedSpectrumConnectedRestriction
Nyll.SchemeTheory.Morphisms.DominantBaseChange
Nyll.SchemeTheory.Normalization.FiniteSeparable
Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Mathlib.Topology.Connected.Basic

Imported by2

instance

fieldSpecQuasiCompact

L37 ↗

EtaleFundamentalGroups.fieldSpecQuasiCompact

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u

Lean source · full declaration

instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

theorem

etale_fieldSourceNormalization_of_finiteEtale_genericFiber

L45 ↗

EtaleFundamentalGroups.etale_fieldSourceNormalization_of_finiteEtale_genericFiber

Documentation

A finite étale model with actual generic fiber Spec L makes the normalization of the base in L étale. No connectedness or comparison of function fields is an additional hypothesis.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits TopologicalSpace
open CategoryTheory.PreGaloisCategory
namespace EtaleFundamentalGroups
universe u
private local instance fieldSpecQuasiCompact
    {K : Type u} [Field K] {S : Scheme.{u}} (f : Spec (.of K) ⟶ S) :
    QuasiCompact f where
  isCompact_preimage U _ _ := (Set.toFinite (f ⁻¹' U)).isCompact

Lean source · statement

theorem etale_fieldSourceNormalization_of_finiteEtale_genericFiber
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (F L : Type u) [Field F] [Field L] [Algebra F L]
    (j : Spec (.of F) ⟶ X) [IsDominant j] [IsPreimmersion j]
    {Y : Scheme.{u}} (f : Y ⟶ X) [IsFinite f] [Etale f]
    (p : Spec (.of L) ⟶ Y)
    (H : IsPullback p (Spec.map (CommRingCat.ofHom (algebraMap F L)))
      f j) :
    Etale (Spec.map (CommRingCat.ofHom (algebraMap F L)) ≫ j).fromNormalization

Module documentation

Normalization at a supplied generic field source

Declarations

fieldSpecQuasiCompact

etale_fieldSourceNormalization_of_finiteEtale_genericFiber