NYLL
Module

Basic.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Basic
22 declarations indexed from sourceView source ↗

Module documentation

Abhyankar's lemma over an arbitrary discrete valuation ring

This file packages the SGA 1 inertia-group argument prime by prime. The base DVR is neither assumed complete nor henselian. All maximal ideals of the normalization in the compositum are quantified, and the conclusion records both inertia restriction exact sequences as well as unramifiedness over the right-hand normalization.

Imports5
Imported by2

Declarations

instance

abhyankarDVRDedekind

L44 ↗
TameAbhyankar.SGA1.abhyankarDVRDedekind
Source context 14 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
Lean source · statement
instance abhyankarDVRDedekind : IsDedekindDomain V
instance

abhyankarLeftSeparable

L47 ↗
TameAbhyankar.SGA1.abhyankarLeftSeparable
Source context 15 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
Lean source · statement
instance abhyankarLeftSeparable : Algebra.IsSeparable K M
instance

abhyankarRightSeparable

L50 ↗
TameAbhyankar.SGA1.abhyankarRightSeparable
Source context 16 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
Lean source · statement
instance abhyankarRightSeparable : Algebra.IsSeparable K N
instance

abhyankarLeftGalois

L53 ↗
TameAbhyankar.SGA1.abhyankarLeftGalois
Source context 17 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
Lean source · statement
instance abhyankarLeftGalois : IsGalois K M
instance

abhyankarRightGalois

L56 ↗
TameAbhyankar.SGA1.abhyankarRightGalois
Source context 18 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
Lean source · statement
instance abhyankarRightGalois : IsGalois K N
instance

abhyankarLeftNormalizationAlgebra

L59 ↗
TameAbhyankar.SGA1.abhyankarLeftNormalizationAlgebra
Source context 19 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
Lean source · statement
instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E)
instance

abhyankarRightNormalizationAlgebra

L63 ↗
TameAbhyankar.SGA1.abhyankarRightNormalizationAlgebra
Source context 20 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
Lean source · statement
instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E)
instance

abhyankarLeftPrimeLiesOver

L67 ↗
TameAbhyankar.SGA1.abhyankarLeftPrimeLiesOver
Source context 21 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
Lean source · full declaration
instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
instance

abhyankarRightPrimeLiesOver

L73 ↗
TameAbhyankar.SGA1.abhyankarRightPrimeLiesOver
Source context 22 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
Lean source · full declaration
instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
instance

abhyankarLeftBasePrimeLiesOver

L79 ↗
TameAbhyankar.SGA1.abhyankarLeftBasePrimeLiesOver
Source context 23 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
Lean source · full declaration
instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
instance

abhyankarRightBasePrimeLiesOver

L85 ↗
TameAbhyankar.SGA1.abhyankarRightBasePrimeLiesOver
Source context 24 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
Lean source · full declaration
instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
instance

abhyankarLeftPrimeIsMaximal

L91 ↗
TameAbhyankar.SGA1.abhyankarLeftPrimeIsMaximal
Source context 25 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
Lean source · statement
instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

abhyankarRightPrimeIsMaximal

L96 ↗
TameAbhyankar.SGA1.abhyankarRightPrimeIsMaximal
Source context 26 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
Lean source · statement
instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal
instance

abhyankarLeftBasePrimeIsMaximal

L101 ↗
TameAbhyankar.SGA1.abhyankarLeftBasePrimeIsMaximal
Source context 27 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
Lean source · statement
instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal
instance

abhyankarRightBasePrimeIsMaximal

L106 ↗
TameAbhyankar.SGA1.abhyankarRightBasePrimeIsMaximal
Source context 28 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
Lean source · statement
instance abhyankarRightBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal
instance

abhyankarTopNormalizationAction

L111 ↗
TameAbhyankar.SGA1.abhyankarTopNormalizationAction
Source context 29 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance abhyankarRightBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
Lean source · statement
instance abhyankarTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E)
instance

abhyankarLeftNormalizationAction

L115 ↗
TameAbhyankar.SGA1.abhyankarLeftNormalizationAction
Source context 30 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance abhyankarRightBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance abhyankarTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
Lean source · statement
instance abhyankarLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M)
instance

abhyankarRightNormalizationAction

L119 ↗
TameAbhyankar.SGA1.abhyankarRightNormalizationAction
Source context 31 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance abhyankarRightBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance abhyankarTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance abhyankarLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
Lean source · statement
instance abhyankarRightNormalizationAction :
    MulSemiringAction Gal(N/K) (integralClosure V N)
def

IsTameAt

L125 ↗
TameAbhyankar.SGA1.NormalizationInertia.IsTameAt
Documentation

Prime-to-residue-characteristic tameness of the inertia group obtained by contracting a top normalization prime to an intermediate normalization.

Source context 32 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance abhyankarRightBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance abhyankarTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance abhyankarLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
noncomputable local instance abhyankarRightNormalizationAction :
    MulSemiringAction Gal(N/K) (integralClosure V N) :=
  IsIntegralClosure.MulSemiringAction V K N (integralClosure V N)
Lean source · statement
def NormalizationInertia.IsTameAt
    (M : IntermediateField K E)
    [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
    (Q : Ideal (integralClosure V E)) : Prop
theorem

abhyankar_for_all_maximalIdeals_of_dvr

L143 ↗
TameAbhyankar.SGA1.abhyankar_for_all_maximalIdeals_of_dvr
Documentation

SGA 1, Expose X, Lemma 3.6, in its inertia-group form over an arbitrary DVR. Tameness is expressed intrinsically: at every maximal prime above the base, each factor inertia order is prime to the fixed exponential residue characteristic. If the left inertia order divides the right one, then the compositum is unramified over the right factor at that prime.

The conclusion also exposes the two surjective inertia restriction maps and identifies both kernels with their relative inertia groups.

Source context 32 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance abhyankarRightBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance abhyankarTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance abhyankarLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
noncomputable local instance abhyankarRightNormalizationAction :
    MulSemiringAction Gal(N/K) (integralClosure V N) :=
  IsIntegralClosure.MulSemiringAction V K N (integralClosure V N)
Lean source · statement
theorem abhyankar_for_all_maximalIdeals_of_dvr
    (hsup : M ⊔ N = ⊤)
    (hleftTame : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      NormalizationInertia.IsTameAt M Q)
    (hrightTame : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      NormalizationInertia.IsTameAt N Q)
    (hcard : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      Nat.card
          ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).toAddSubgroup.inertia
            Gal(M/K)) ∣
        Nat.card
          ((normalizationLowerPrime (V := V) (K := K) (E := E) N Q).toAddSubgroup.inertia
            Gal(N/K)))
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
      Function.Surjective (normalizationInertiaRestriction (V := V) M Q) ∧
      MonoidHom.ker (normalizationInertiaRestriction (V := V) M Q) =
        (idealRelativeInertiaInclusion (Q := Q)
          (normalizationRestrictionHom M)).range ∧
      Function.Surjective (normalizationInertiaRestriction (V := V) N Q) ∧
      MonoidHom.ker (normalizationInertiaRestriction (V := V) N Q) =
        (idealRelativeInertiaInclusion (Q := Q)
          (normalizationRestrictionHom N)).range ∧
      Nat.card
          (Q.toAddSubgroup.inertia
            (normalizationRestrictionHom N).ker) = 1 ∧
      Algebra.IsUnramifiedAt (integralClosure V N) Q
theorem

abhyankar_isUnramifiedAt_all_maximalIdeals_of_dvr

L285 ↗
TameAbhyankar.SGA1.abhyankar_isUnramifiedAt_all_maximalIdeals_of_dvr
Documentation

The unramifiedness-only form of Abhyankar's lemma. Its conclusion is explicitly quantified over every maximal ideal, hence over every localization of the right-hand normalization.

Source context 32 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance abhyankarRightBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance abhyankarTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance abhyankarLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
noncomputable local instance abhyankarRightNormalizationAction :
    MulSemiringAction Gal(N/K) (integralClosure V N) :=
  IsIntegralClosure.MulSemiringAction V K N (integralClosure V N)
Lean source · statement
theorem abhyankar_isUnramifiedAt_all_maximalIdeals_of_dvr
    (hsup : M ⊔ N = ⊤)
    (hleftTame : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      NormalizationInertia.IsTameAt M Q)
    (hrightTame : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      NormalizationInertia.IsTameAt N Q)
    (hcard : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      Nat.card
          ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).toAddSubgroup.inertia
            Gal(M/K)) ∣
        Nat.card
          ((normalizationLowerPrime (V := V) (K := K) (E := E) N Q).toAddSubgroup.inertia
            Gal(N/K))) :
    ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      Algebra.IsUnramifiedAt (integralClosure V N) Q
theorem

abhyankar_isUnramifiedAt_all_localizations_of_dvr

L308 ↗
TameAbhyankar.SGA1.abhyankar_isUnramifiedAt_all_localizations_of_dvr
Documentation

SGA 1's localization formulation: for every maximal ideal P of the right-hand normalization and every maximal ideal Q of the compositum normalization lying over it, the localized extension is unramified at Q.

Source context 32 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
variable [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [FiniteDimensional K E] [IsGalois K E]
variable (M N : IntermediateField K E)
variable [Normal K M] [Normal K N]
variable [Algebra V M] [IsScalarTower V K M] [IsScalarTower V M E]
variable [Algebra V N] [IsScalarTower V K N] [IsScalarTower V N E]
local instance abhyankarDVRDedekind : IsDedekindDomain V :=
  isDedekindDomain_of_isDiscreteValuationRing V
local instance abhyankarLeftSeparable : Algebra.IsSeparable K M :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) M E
local instance abhyankarRightSeparable : Algebra.IsSeparable K N :=
  Algebra.isSeparable_tower_bot_of_isSeparable (F := K) N E
local instance abhyankarLeftGalois : IsGalois K M :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarRightGalois : IsGalois K N :=
  isGalois_iff.mpr ⟨inferInstance, inferInstance⟩
local instance abhyankarLeftNormalizationAlgebra :
    Algebra (integralClosure V M) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) M
local instance abhyankarRightNormalizationAlgebra :
    Algebra (integralClosure V N) (integralClosure V E) :=
  normalizationAlgebra (V := V) (K := K) (E := E) N
local instance abhyankarLeftPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightPrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    Q.LiesOver
      (normalizationLowerPrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) M Q) where
  over := rfl
local instance abhyankarRightBasePrimeLiesOver
    (Q : Ideal (integralClosure V E)) :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).LiesOver
      (normalizationBasePrime (V := V) (K := K) (E := E) N Q) where
  over := rfl
local instance abhyankarLeftPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) M Q
local instance abhyankarRightPrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationLowerPrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationLowerPrime_isMaximal (V := V) N Q
local instance abhyankarLeftBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) M Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) M Q
local instance abhyankarRightBasePrimeIsMaximal
    (Q : Ideal (integralClosure V E)) [Q.IsMaximal] :
    (normalizationBasePrime (V := V) (K := K) (E := E) N Q).IsMaximal :=
  normalizationBasePrime_isMaximal (V := V) N Q
noncomputable local instance abhyankarTopNormalizationAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance abhyankarLeftNormalizationAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
noncomputable local instance abhyankarRightNormalizationAction :
    MulSemiringAction Gal(N/K) (integralClosure V N) :=
  IsIntegralClosure.MulSemiringAction V K N (integralClosure V N)
Lean source · statement
theorem abhyankar_isUnramifiedAt_all_localizations_of_dvr
    (hsup : M ⊔ N = ⊤)
    (hleftTame : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      NormalizationInertia.IsTameAt M Q)
    (hrightTame : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      NormalizationInertia.IsTameAt N Q)
    (hcard : ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
      Nat.card
          ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).toAddSubgroup.inertia
            Gal(M/K)) ∣
        Nat.card
          ((normalizationLowerPrime (V := V) (K := K) (E := E) N Q).toAddSubgroup.inertia
            Gal(N/K))) :
    ∀ (P : Ideal (integralClosure V N)), [P.IsMaximal] →
      ∀ (Q : Ideal (integralClosure V E)), [Q.IsMaximal] →
        [Q.LiesOver P] → Algebra.IsUnramifiedAt (integralClosure V N) Q

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