NYLL
Module

FiniteEtaleGaloisCoverNormalizationAction.lean

Nyll.EtaleFundamentalGroups.Kummer.Normalization.FiniteEtaleGaloisCoverNormalizationAction
3 declarations indexed from sourceView source ↗

Module documentation

Normalization actions of finite-etale Galois-cover quotients

For a finite-etale Galois cover of a normal integral locally Noetherian scheme, the opposite categorical automorphism group is the Galois group of the induced function-field extension. This file transports the canonical normalization-ring action across that equivalence.

Imports2
Imported by5

Declarations

def

finiteEtaleGaloisCoverNormalizationAction

L33 ↗
EtaleFundamentalGroups.Kummer.finiteEtaleGaloisCoverNormalizationAction
Documentation

The action of the categorical Galois-cover quotient on a normalization ring, transported from the function-field Galois action.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped Pointwise
namespace EtaleFundamentalGroups.Kummer
universe u uA uB
Lean source · full declaration
def finiteEtaleGaloisCoverNormalizationAction
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (Y : FiniteEtale X) (hY : IsGalois Y) :
    letI : IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    let K := X.functionField
    let L := Y.left.functionField
    letI : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
    ∀ (A : Type uA) (B : Type uB)
      [CommRing A] [CommRing B]
      [Algebra A K] [IsFractionRing A K]
      [Algebra B L] [IsFractionRing B L]
      [Algebra A B] [Algebra A L]
      [IsScalarTower A K L] [IsScalarTower A B L]
      [IsIntegrallyClosed A] [IsIntegralClosure B A L],
      MulSemiringAction (Aut Y)ᵐᵒᵖ B := by
  letI : IsGalois Y := hY
  letI : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let K := X.functionField
  let L := Y.left.functionField
  letI : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
  dsimp only
  intro A B _ _ _ _ _ _ _ _ _ _ _ _
  letI : FiniteDimensional K L :=
    finiteDimensional_functionField_of_finiteEtale_isConnected Y
  letI : MulSemiringAction Gal(L/K) B :=
    IsIntegralClosure.MulSemiringAction A K L B
  exact MulSemiringAction.compHom B
    (finiteEtaleAutOpFunctionFieldMulEquiv Y hY).toMonoidHom
theorem

finiteEtaleGaloisCoverNormalizationAction_smul

L68 ↗
EtaleFundamentalGroups.Kummer.finiteEtaleGaloisCoverNormalizationAction_smul
Documentation

The transported categorical action agrees pointwise with the canonical function-field Galois action on the normalization.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped Pointwise
namespace EtaleFundamentalGroups.Kummer
universe u uA uB
Lean source · full declaration
theorem finiteEtaleGaloisCoverNormalizationAction_smul
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (Y : FiniteEtale X) (hY : IsGalois Y) :
    letI : IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    let K := X.functionField
    let L := Y.left.functionField
    letI : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
    ∀ (A : Type uA) (B : Type uB)
      [CommRing A] [CommRing B]
      [Algebra A K] [IsFractionRing A K]
      [Algebra B L] [IsFractionRing B L]
      [Algebra A B] [Algebra A L]
      [IsScalarTower A K L] [IsScalarTower A B L]
      [IsIntegrallyClosed A] [IsIntegralClosure B A L]
      (sigma : (Aut Y)ᵐᵒᵖ) (b : B),
      letI : FiniteDimensional K L :=
        finiteDimensional_functionField_of_finiteEtale_isConnected Y
      letI : MulSemiringAction Gal(L/K) B :=
        IsIntegralClosure.MulSemiringAction A K L B
      letI : MulSemiringAction (Aut Y)ᵐᵒᵖ B :=
        finiteEtaleGaloisCoverNormalizationAction Y hY A B
      (finiteEtaleAutOpFunctionFieldMulEquiv Y hY sigma) • b = sigma • b := by
  let : IsGalois Y := hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let K := X.functionField
  let L := Y.left.functionField
  let : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
  dsimp only
  intro A B _ _ _ _ _ _ _ _ _ _ _ _ sigma b
  rfl
theorem

finiteEtaleGaloisCoverNormalizationSMulCommClass

L105 ↗
EtaleFundamentalGroups.Kummer.finiteEtaleGaloisCoverNormalizationSMulCommClass
Documentation

The categorical cover action on the normalization commutes with the base-ring scalar action.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
open CategoryTheory.PreGaloisCategory
open scoped Pointwise
namespace EtaleFundamentalGroups.Kummer
universe u uA uB
Lean source · full declaration
theorem finiteEtaleGaloisCoverNormalizationSMulCommClass
    {X : Scheme.{u}} [IsIntegral X] [IsNormalIntegral X]
    [IsLocallyNoetherian X]
    (Y : FiniteEtale X) (hY : IsGalois Y) :
    letI : IsGalois Y := hY
    letI : IsIntegral Y.left :=
      isIntegral_left_of_isConnected_finiteEtale Y
    let K := X.functionField
    let L := Y.left.functionField
    letI : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
    ∀ (A : Type uA) (B : Type uB)
      [CommRing A] [CommRing B]
      [Algebra A K] [IsFractionRing A K]
      [Algebra B L] [IsFractionRing B L]
      [Algebra A B] [Algebra A L]
      [IsScalarTower A K L] [IsScalarTower A B L]
      [IsIntegrallyClosed A] [IsIntegralClosure B A L],
      letI : FiniteDimensional K L :=
        finiteDimensional_functionField_of_finiteEtale_isConnected Y
      letI : MulSemiringAction Gal(L/K) B :=
        IsIntegralClosure.MulSemiringAction A K L B
      letI : MulSemiringAction (Aut Y)ᵐᵒᵖ B :=
        finiteEtaleGaloisCoverNormalizationAction Y hY A B
      SMulCommClass (Aut Y)ᵐᵒᵖ A B := by
  let : IsGalois Y := hY
  let : IsIntegral Y.left :=
    isIntegral_left_of_isConnected_finiteEtale Y
  let K := X.functionField
  let L := Y.left.functionField
  let : Algebra K L := finiteEtaleFunctionFieldAlgebra Y
  dsimp only
  intro A B _ _ _ _ _ _ _ _ _ _ _ _
  let : FiniteDimensional K L :=
    finiteDimensional_functionField_of_finiteEtale_isConnected Y
  let : MulSemiringAction Gal(L/K) B :=
    IsIntegralClosure.MulSemiringAction A K L B
  let : MulSemiringAction (Aut Y)ᵐᵒᵖ B :=
    finiteEtaleGaloisCoverNormalizationAction Y hY A B
  constructor
  intro sigma a b
  change galRestrict A K L B
      (finiteEtaleAutOpFunctionFieldMulEquiv Y hY sigma) (a • b) =
    a • galRestrict A K L B
      (finiteEtaleAutOpFunctionFieldMulEquiv Y hY sigma) b
  exact map_smul (galRestrict A K L B
    (finiteEtaleAutOpFunctionFieldMulEquiv Y hY sigma)) a b

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