NYLL
Module

FunctionField.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.FunctionField
6 declarations indexed from sourceView source ↗

Module documentation

Function fields of connected finite-etale covers

A connected finite-etale cover of a normal integral scheme has a canonical finite separable extension of function fields.

Imports2
Imported by6

Declarations

theorem

finiteEtale_hom_denseRange_of_isConnected

L29 ↗
EtaleFundamentalGroups.finiteEtale_hom_denseRange_of_isConnected
Documentation

The structure morphism of a connected finite-etale cover of an integral scheme has dense image.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
Lean source · statement
theorem finiteEtale_hom_denseRange_of_isConnected
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (Y : FiniteEtale X) [IsConnected Y] : DenseRange Y.hom
def

finiteEtaleFunctionFieldAlgebra

L46 ↗
EtaleFundamentalGroups.finiteEtaleFunctionFieldAlgebra
Documentation

The canonical algebra structure on the function field of a connected finite-etale cover.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
Lean source · full declaration
def finiteEtaleFunctionFieldAlgebra
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (Y : FiniteEtale X) [IsConnected Y] :
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    Algebra X.functionField Y.left.functionField := by
  letI : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  exact ((show Y.left ⟶ X from Y.hom).functionFieldMap
    (finiteEtale_hom_denseRange_of_isConnected Y)).toAlgebra
theorem

finiteEtale_functionFieldMap_essFiniteType

L59 ↗
EtaleFundamentalGroups.finiteEtale_functionFieldMap_essFiniteType
Documentation

The canonical function-field map of a connected finite-etale cover is essentially of finite type.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
Lean source · full declaration
theorem finiteEtale_functionFieldMap_essFiniteType
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (Y : FiniteEtale X) [IsConnected Y] :
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    ((show Y.left ⟶ X from Y.hom).functionFieldMap
      (finiteEtale_hom_denseRange_of_isConnected Y)).EssFiniteType := by
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : IsFiniteEtale (show Y.left ⟶ X from Y.hom) := Y.2
  unfold Scheme.Hom.functionFieldMap
  rw [CommRingCat.hom_comp,
    RingHom.EssFiniteType.respectsIso.cancel_left_isIso]
  exact LocallyOfFiniteType.stalkMap
    (show Y.left ⟶ X from Y.hom) (genericPoint Y.left)
theorem

finiteEtale_functionFieldMap_formallyUnramified

L77 ↗
EtaleFundamentalGroups.finiteEtale_functionFieldMap_formallyUnramified
Documentation

The canonical function-field map of a connected finite-etale cover is formally unramified.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
Lean source · full declaration
theorem finiteEtale_functionFieldMap_formallyUnramified
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (Y : FiniteEtale X) [IsConnected Y] :
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    ((show Y.left ⟶ X from Y.hom).functionFieldMap
      (finiteEtale_hom_denseRange_of_isConnected Y)).FormallyUnramified := by
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : IsFiniteEtale (show Y.left ⟶ X from Y.hom) := Y.2
  unfold Scheme.Hom.functionFieldMap
  rw [CommRingCat.hom_comp,
    RingHom.FormallyUnramified.respectsIso.cancel_left_isIso]
  exact FormallyUnramified.stalkMap
    (show Y.left ⟶ X from Y.hom) (genericPoint Y.left)
theorem

finiteDimensional_functionField_of_finiteEtale_isConnected

L95 ↗
EtaleFundamentalGroups.finiteDimensional_functionField_of_finiteEtale_isConnected
Documentation

A connected finite-etale cover induces a finite-dimensional extension of function fields.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
Lean source · full declaration
theorem finiteDimensional_functionField_of_finiteEtale_isConnected
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (Y : FiniteEtale X) [IsConnected Y] :
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    letI : Algebra X.functionField Y.left.functionField :=
      finiteEtaleFunctionFieldAlgebra Y
    FiniteDimensional X.functionField Y.left.functionField := by
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : Algebra X.functionField Y.left.functionField :=
    finiteEtaleFunctionFieldAlgebra Y
  let : Algebra.EssFiniteType X.functionField Y.left.functionField := by
    apply RingHom.essFiniteType_algebraMap.mp
    change ((show Y.left ⟶ X from Y.hom).functionFieldMap
      (finiteEtale_hom_denseRange_of_isConnected Y)).EssFiniteType
    exact finiteEtale_functionFieldMap_essFiniteType Y
  let : Algebra.FormallyUnramified X.functionField Y.left.functionField := by
    apply RingHom.formallyUnramified_algebraMap.mp
    change ((show Y.left ⟶ X from Y.hom).functionFieldMap
      (finiteEtale_hom_denseRange_of_isConnected Y)).FormallyUnramified
    exact finiteEtale_functionFieldMap_formallyUnramified Y
  exact Algebra.FormallyUnramified.finite_of_free
    X.functionField Y.left.functionField
theorem

isSeparable_functionField_of_finiteEtale_isConnected

L122 ↗
EtaleFundamentalGroups.isSeparable_functionField_of_finiteEtale_isConnected
Documentation

A connected finite-etale cover induces a separable extension of function fields.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
open CategoryTheory.PreGaloisCategory
open AlgebraicGeometry
namespace EtaleFundamentalGroups
universe u
Lean source · full declaration
theorem isSeparable_functionField_of_finiteEtale_isConnected
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    (Y : FiniteEtale X) [IsConnected Y] :
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    letI : Algebra X.functionField Y.left.functionField :=
      finiteEtaleFunctionFieldAlgebra Y
    Algebra.IsSeparable X.functionField Y.left.functionField := by
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let : Algebra X.functionField Y.left.functionField :=
    finiteEtaleFunctionFieldAlgebra Y
  let : Algebra.EssFiniteType X.functionField Y.left.functionField := by
    apply RingHom.essFiniteType_algebraMap.mp
    change ((show Y.left ⟶ X from Y.hom).functionFieldMap
      (finiteEtale_hom_denseRange_of_isConnected Y)).EssFiniteType
    exact finiteEtale_functionFieldMap_essFiniteType Y
  let : Algebra.FormallyUnramified X.functionField Y.left.functionField := by
    apply RingHom.formallyUnramified_algebraMap.mp
    change ((show Y.left ⟶ X from Y.hom).functionFieldMap
      (finiteEtale_hom_denseRange_of_isConnected Y)).FormallyUnramified
    exact finiteEtale_functionFieldMap_formallyUnramified Y
  exact Algebra.FormallyUnramified.isSeparable
    X.functionField Y.left.functionField

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