Module

Tame.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Normalization.Tame

4 declarations indexed from sourceView source ↗

Module documentation

Tameness at a prime of a normalization compositum

The inertia group at a prime of a compositum embeds in the product of the two factor inertia groups. Consequently, prime-to-residue-characteristic tameness of both factors propagates to the compositum, prime by prime.

Imports3

Imported by2

instance

normalizationTameTopAction

L36 ↗

TameAbhyankar.SGA1.normalizationTameTopAction

Source context 12 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [IsDedekindDomain V] [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 normalizationTameTopAction :
    MulSemiringAction Gal(E/K) (integralClosure V E)

instance

normalizationTameLeftAction

L40 ↗

TameAbhyankar.SGA1.normalizationTameLeftAction

Source context 13 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [IsDedekindDomain V] [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]
noncomputable local instance normalizationTameTopAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)

Lean source · statement

instance normalizationTameLeftAction :
    MulSemiringAction Gal(M/K) (integralClosure V M)

instance

normalizationTameRightAction

L44 ↗

TameAbhyankar.SGA1.normalizationTameRightAction

Source context 14 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [IsDedekindDomain V] [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]
noncomputable local instance normalizationTameTopAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance normalizationTameLeftAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)

Lean source · statement

instance normalizationTameRightAction :
    MulSemiringAction Gal(N/K) (integralClosure V N)

theorem

normalizationTopInertia_card_coprime

L51 ↗

TameAbhyankar.SGA1.normalizationTopInertia_card_coprime

Documentation

At every prime of the top normalization, the top inertia order is prime to p if the inertia orders at both contractions are prime to p.

Source context 16 commands

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

noncomputable section
universe uV uK uE
namespace TameAbhyankar.SGA1
variable {V : Type uV} {K : Type uK} {E : Type uE}
variable [CommRing V] [Field K] [Field E]
variable [Algebra V K] [IsFractionRing V K]
variable [Algebra K E] [Algebra V E] [IsScalarTower V K E]
variable [IsDedekindDomain V] [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]
noncomputable local instance normalizationTameTopAction :
    MulSemiringAction Gal(E/K) (integralClosure V E) :=
  IsIntegralClosure.MulSemiringAction V K E (integralClosure V E)
noncomputable local instance normalizationTameLeftAction :
    MulSemiringAction Gal(M/K) (integralClosure V M) :=
  IsIntegralClosure.MulSemiringAction V K M (integralClosure V M)
noncomputable local instance normalizationTameRightAction :
    MulSemiringAction Gal(N/K) (integralClosure V N) :=
  IsIntegralClosure.MulSemiringAction V K N (integralClosure V N)
omit [IsDedekindDomain V] in

Lean source · statement

theorem normalizationTopInertia_card_coprime
    (hsup : M ⊔ N = ⊤)
    (Q : Ideal (integralClosure V E))
    (p : ℕ)
    (hleft : Nat.Coprime
      (Nat.card
        ((normalizationLowerPrime (V := V) (K := K) (E := E) M Q).toAddSubgroup.inertia
          Gal(M/K))) p)
    (hright : Nat.Coprime
      (Nat.card
        ((normalizationLowerPrime (V := V) (K := K) (E := E) N Q).toAddSubgroup.inertia
          Gal(N/K))) p) :
    Nat.Coprime
      (Nat.card (Q.toAddSubgroup.inertia Gal(E/K))) p

Module documentation

Tameness at a prime of a normalization compositum

Declarations

normalizationTameTopAction

normalizationTameLeftAction

normalizationTameRightAction

normalizationTopInertia_card_coprime