NYLL
Module

AffineUnramifiedSubfield.lean

Nyll.EtaleFundamentalGroups.Normalization.AffineUnramifiedSubfield
8 declarations indexed from sourceView source ↗

Module documentation

The original maximal unramified subextension over a normal domain

The field is defined as the supremum of the finite subfields of the supplied ambient field whose literal integral closures over A are unramified. The geometric criterion then proves that this is the field fixed by the actual fundamental-group kernel, and that its elements form the literal union.

Imports8
Imported by2

Declarations

def

maximalUnramifiedSubfield

L37 ↗
EtaleFundamentalGroups.maximalUnramifiedSubfield
Documentation

The maximal subextension unramified over A, using finite subfields of the original supplied ambient field and their actual integral closures.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v w
Lean source · statement
def maximalUnramifiedSubfield
    (A : Type u) (K : Type v) (Ω : Type w) [CommRing A] [Field K] [Field Ω]
    [Algebra A K] [Algebra K Ω] [Algebra A Ω] [IsScalarTower A K Ω] :
    IntermediateField K Ω
instance

fieldSpecQuasiCompact

L45 ↗
EtaleFundamentalGroups.fieldSpecQuasiCompact
Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v w
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
instance

fractionSourcePreimmersion

L50 ↗
EtaleFundamentalGroups.fractionSourcePreimmersion
Source context 7 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v w
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
instance fractionSourcePreimmersion
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsPreimmersion (Spec.map (CommRingCat.ofHom (algebraMap A F)))
instance

fractionSourceDominant

L56 ↗
EtaleFundamentalGroups.fractionSourceDominant
Source context 8 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v w
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
private local instance fractionSourcePreimmersion
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsPreimmersion (Spec.map (CommRingCat.ofHom (algebraMap A F))) :=
  IsPreimmersion.of_isLocalization A⁰
Lean source · statement
instance fractionSourceDominant
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsDominant (Spec.map (CommRingCat.ofHom (algebraMap A F)))
theorem

integralClosure_etale_iff_fieldSourceKernel_le_fixingSubgroup

L73 ↗
EtaleFundamentalGroups.integralClosure_etale_iff_fieldSourceKernel_le_fixingSubgroup
Documentation

The normalization of a literal finite subfield is étale exactly when the actual generic fundamental-group kernel fixes that subfield.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v w
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
private local instance fractionSourcePreimmersion
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsPreimmersion (Spec.map (CommRingCat.ofHom (algebraMap A F))) :=
  IsPreimmersion.of_isLocalization A⁰
private local instance fractionSourceDominant
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsDominant (Spec.map (CommRingCat.ofHom (algebraMap A F))) := by
  rw [isDominant_iff]
  change DenseRange (PrimeSpectrum.comap (algebraMap A F))
  apply (PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical _).mpr
  rw [(RingHom.injective_iff_ker_eq_bot _).mp (IsFractionRing.injective A F)]
  exact bot_le
variable (A F Ω : Type u) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field F] [Field Ω] [Algebra A F] [IsFractionRing A F]
  [Algebra F Ω] [Algebra A Ω] [IsScalarTower A F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
Lean source · statement
theorem integralClosure_etale_iff_fieldSourceKernel_le_fixingSubgroup
    (E : IntermediateField F Ω) [FiniteDimensional F E] :
    Algebra.Etale A (integralClosure A E) ↔
      (fieldSourceAbsoluteGaloisHom F Ω
        (Spec.map (CommRingCat.ofHom (algebraMap A F)))).toMonoidHom.ker ≤
          E.fixingSubgroup
theorem

integralClosure_unramified_iff_fieldSourceKernel_le_fixingSubgroup

L137 ↗
EtaleFundamentalGroups.integralClosure_unramified_iff_fieldSourceKernel_le_fixingSubgroup
Documentation

Unramifiedness uses the literal integral closure, with no finiteness of normalization assumed: finite type and formal unramifiedness imply étaleness.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v w
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
private local instance fractionSourcePreimmersion
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsPreimmersion (Spec.map (CommRingCat.ofHom (algebraMap A F))) :=
  IsPreimmersion.of_isLocalization A⁰
private local instance fractionSourceDominant
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsDominant (Spec.map (CommRingCat.ofHom (algebraMap A F))) := by
  rw [isDominant_iff]
  change DenseRange (PrimeSpectrum.comap (algebraMap A F))
  apply (PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical _).mpr
  rw [(RingHom.injective_iff_ker_eq_bot _).mp (IsFractionRing.injective A F)]
  exact bot_le
variable (A F Ω : Type u) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field F] [Field Ω] [Algebra A F] [IsFractionRing A F]
  [Algebra F Ω] [Algebra A Ω] [IsScalarTower A F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
Lean source · statement
theorem integralClosure_unramified_iff_fieldSourceKernel_le_fixingSubgroup
    (E : IntermediateField F Ω) [FiniteDimensional F E] :
    (Algebra.FormallyUnramified A (integralClosure A E) ∧
      Algebra.FiniteType A (integralClosure A E)) ↔
      (fieldSourceAbsoluteGaloisHom F Ω
        (Spec.map (CommRingCat.ofHom (algebraMap A F)))).toMonoidHom.ker ≤
          E.fixingSubgroup
theorem

mem_fieldSourceKernelFixedField_iff_exists_unramified_finite_subfield

L164 ↗
EtaleFundamentalGroups.mem_fieldSourceKernelFixedField_iff_exists_unramified_finite_subfield
Documentation

The fixed field of the actual generic kernel is the literal union of finite subextensions unramified over A in the given ambient field.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v w
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
private local instance fractionSourcePreimmersion
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsPreimmersion (Spec.map (CommRingCat.ofHom (algebraMap A F))) :=
  IsPreimmersion.of_isLocalization A⁰
private local instance fractionSourceDominant
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsDominant (Spec.map (CommRingCat.ofHom (algebraMap A F))) := by
  rw [isDominant_iff]
  change DenseRange (PrimeSpectrum.comap (algebraMap A F))
  apply (PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical _).mpr
  rw [(RingHom.injective_iff_ker_eq_bot _).mp (IsFractionRing.injective A F)]
  exact bot_le
variable (A F Ω : Type u) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field F] [Field Ω] [Algebra A F] [IsFractionRing A F]
  [Algebra F Ω] [Algebra A Ω] [IsScalarTower A F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
Lean source · statement
theorem mem_fieldSourceKernelFixedField_iff_exists_unramified_finite_subfield
    (x : Ω) :
    x ∈ IntermediateField.fixedField
      (fieldSourceAbsoluteGaloisHom F Ω
        (Spec.map (CommRingCat.ofHom (algebraMap A F)))).toMonoidHom.ker ↔
      ∃ E : IntermediateField F Ω, FiniteDimensional F E ∧
        (Algebra.FormallyUnramified A (integralClosure A E) ∧
          Algebra.FiniteType A (integralClosure A E)) ∧ x ∈ E
theorem

maximalUnramifiedSubfield_eq_fieldSourceKernelFixedField

L193 ↗
EtaleFundamentalGroups.maximalUnramifiedSubfield_eq_fieldSourceKernelFixedField
Documentation

The independently defined maximal unramified subfield equals the fixed field of the actual fundamental-group kernel.

Source context 10 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open AlgebraicGeometry.FiniteEtale
open scoped nonZeroDivisors
namespace EtaleFundamentalGroups
universe u v w
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
private local instance fractionSourcePreimmersion
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsPreimmersion (Spec.map (CommRingCat.ofHom (algebraMap A F))) :=
  IsPreimmersion.of_isLocalization A⁰
private local instance fractionSourceDominant
    (A F : Type u) [CommRing A] [IsDomain A] [Field F]
    [Algebra A F] [IsFractionRing A F] :
    IsDominant (Spec.map (CommRingCat.ofHom (algebraMap A F))) := by
  rw [isDominant_iff]
  change DenseRange (PrimeSpectrum.comap (algebraMap A F))
  apply (PrimeSpectrum.denseRange_comap_iff_ker_le_nilRadical _).mpr
  rw [(RingHom.injective_iff_ker_eq_bot _).mp (IsFractionRing.injective A F)]
  exact bot_le
variable (A F Ω : Type u) [CommRing A] [IsDomain A] [IsIntegrallyClosed A]
  [Field F] [Field Ω] [Algebra A F] [IsFractionRing A F]
  [Algebra F Ω] [Algebra A Ω] [IsScalarTower A F Ω]
  [IsSepClosure F Ω] [IsSepClosed Ω]
Lean source · statement
theorem maximalUnramifiedSubfield_eq_fieldSourceKernelFixedField :
    maximalUnramifiedSubfield A F Ω = IntermediateField.fixedField
      (fieldSourceAbsoluteGaloisHom F Ω
        (Spec.map (CommRingCat.ofHom (algebraMap A F)))).toMonoidHom.ker

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.