ActualFiniteTameOrderTower.lean

theorem finiteNormalization_tame_arithmetic
    (A : Type u) (K : Type v) (C : Type w)
    [rA : CommRing A] [dA : IsDomain A] [vA : IsDiscreteValuationRing A]
    [fK : Field K] [fC : Field C]
    [aAK : Algebra A K] [fAK : IsFractionRing A K]
    [aKC : Algebra K C] [aAC : Algebra A C] [tAKC : IsScalarTower A K C]
    [fKC : FiniteDimensional K C] [gKC : IsGalois K C] :
    letI : IsDedekindDomain (normalizationCommAlgCat A C) :=
      integralClosure.isDedekindDomain A K C
    ∀ (Q : Ideal (normalizationCommAlgCat A C)) [_qPrime : Q.IsPrime] (hQ : Q ≠ ⊥),
      commAlgIdealTameOrder A (normalizationCommAlgCat A C) Q hQ ∣ Q.ramificationIdx A ∧
      ∀ n : ℕ, IsUnit (n : A) →
        Nat.Coprime n (Q.ramificationIdx A /
          commAlgIdealTameOrder A (normalizationCommAlgCat A C) Q hQ) := by
  let B : CommAlgCat.{w} A := normalizationCommAlgCat A C
  have dB : IsDedekindDomain B := integralClosure.isDedekindDomain A K C
  have tAC : Module.IsTorsionFree A C := .trans_faithfulSMul A K C
  have tAB : Module.IsTorsionFree A B :=
    inferInstanceAs (Module.IsTorsionFree A (integralClosure A C))
  have fAB : Module.Finite A B :=
    nativeNormalization_finite A K (CommAlgCat.of A C) (Field.toIsField C)
  have gAB : IsGaloisGroup (B ≃ₐ[A] B) A B :=
    integralClosure_automorphisms_isGaloisGroup A K C
  change ∀ (Q : Ideal B) [Q.IsPrime] (hQ : Q ≠ ⊥),
    commAlgIdealTameOrder A B Q hQ ∣ Q.ramificationIdx A ∧
      ∀ n : ℕ, IsUnit (n : A) →
        Nat.Coprime n (Q.ramificationIdx A / commAlgIdealTameOrder A B Q hQ)
  clear_value B
  clear tAC gKC fKC tAKC aAC aKC fAK aAK fC C fK K
  intro Q qPrime hQ
  have hmax : Q.IsMaximal := Ideal.IsPrime.isMaximal qPrime hQ
  have hbaseMax : (Q.under A).IsMaximal :=
    Ideal.isMaximal_under_of_isIntegral_of_isMaximal Q
  have hover : Q.LiesOver (IsLocalRing.maximalIdeal A) :=
    ⟨(IsLocalRing.eq_maximalIdeal hbaseMax).symm⟩
  constructor
  · exact finiteIdealTameOrder_dvd_ramificationIdx A B (B ≃ₐ[A] B) Q hQ
  · intro n hn
    exact finiteIdealNormalizationExponent_coprime_of_isUnit_base A B Q hQ n hn

theorem actualFiniteStage_tame_arithmetic
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]
    (E : FiniteGaloisIntermediateField K L) :
    actualFiniteStageTameOrder A K L Q E ∣
        (finiteAbsoluteNormalizationPrime A K L Q E).ramificationIdx A ∧
      ∀ n : ℕ, IsUnit (n : A) → Nat.Coprime n
        ((finiteAbsoluteNormalizationPrime A K L Q E).ramificationIdx A /
          actualFiniteStageTameOrder A K L Q E)

theorem actualFiniteStageTameOrder_dvd_of_le
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
    [Field K] [Field L] [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (normalizationCommAlgCat A L)) [Q.IsMaximal]
    (E F : FiniteGaloisIntermediateField K L) (h : E ≤ F) :
    actualFiniteStageTameOrder A K L Q E ∣ actualFiniteStageTameOrder A K L Q F