Place_ramificationIndex_mul_inertiaDeg_mul_natCard_stabilizer_eq_natCard_stabilizer.lean

theorem ord_coe_eq_of_eq_unit_mul_pow (w : Place K F') {x ϖ : w.toValuationSubring}
    (hϖ : Irreducible ϖ) {u : w.toValuationSubringˣ} {m : ℕ} (hx : x = u * ϖ ^ m) :
    w.ord (x : F') = m

theorem mem_maximalIdeal_pow_iff (w : Place K F') {x : w.toValuationSubring} (hx : x ≠ 0) (n : ℕ) :
    x ∈ maximalIdeal w.toValuationSubring ^ n ↔ (n : ℤ) ≤ w.ord (x : F')

theorem one_le_ord_of_mem_maximalIdeal (w : Place K F') {x : w.toValuationSubring} (hx0 : x ≠ 0)
    (hx : x ∈ maximalIdeal w.toValuationSubring) : 1 ≤ w.ord (x : F')

theorem restrictInclusion_ne_zero (w : Place K F') {r : (w.restrict F).toValuationSubring} (hr : r
  ≠ 0) :
    Place.restrictInclusion F w r ≠ 0

theorem ramificationIdx_eq_ramificationIndex (w : Place K F') :
    @Ideal.ramificationIdx' _ _ _ _ (Place.restrictInclusion F w).toAlgebra
        (maximalIdeal (w.restrict F).toValuationSubring) (maximalIdeal w.toValuationSubring) =
      w.ramificationIndex F

theorem inertiaDeg_eq_inertiaDeg (w : Place K F') :
    (letI := (Place.restrictInclusion F w).toAlgebra
     (maximalIdeal w.toValuationSubring).inertiaDeg (w.restrict F).toValuationSubring) =
      w.inertiaDeg F := by
  let _ := (Place.restrictInclusion F w).toAlgebra
  have hlo : (maximalIdeal w.toValuationSubring).LiesOver (maximalIdeal (w.restrict
    F).toValuationSubring) :=
    ⟨(IsLocalRing.maximalIdeal_comap (Place.restrictInclusion F w)).symm⟩
  rw [Ideal.inertiaDeg_eq_of_isMaximal
    (maximalIdeal (w.restrict F).toValuationSubring) (maximalIdeal w.toValuationSubring)]
  have h : (inferInstance : Algebra ((w.restrict F).toValuationSubring ⧸ maximalIdeal (w.restrict
    F).toValuationSubring)
      (w.toValuationSubring ⧸ maximalIdeal w.toValuationSubring)) =
      ((Place.restrictResidueMap F w).toAlgebra : Algebra (w.restrict F).ResidueField
        w.ResidueField) := by
    refine Algebra.algebra_ext _ _ fun x => ?_
    obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
    rfl
  unfold Place.inertiaDeg
  exact congrArg (fun I : Algebra ((w.restrict F).toValuationSubring ⧸ maximalIdeal (w.restrict
    F).toValuationSubring)
      (w.toValuationSubring ⧸ maximalIdeal w.toValuationSubring) => @Module.finrank _ _ _ _
        (@Algebra.toModule _ _ _ _ I)) h

theorem stab_iff {k L M : Type*} [Field k] [Field L] [Field M] [Algebra k L] [Algebra k M] [Algebra
  L M]
    [IsScalarTower k L M] (c : Place k M) (σ : M ≃ₐ[L] M) :
    SemilinearAut.ofAlgAut (σ.restrictScalars k) • c = c ↔
      σ ∈ c.toValuationSubring.decompositionSubgroup L

theorem card_stab_eq {k L M : Type*} [Field k] [Field L] [Field M] [Algebra k L] [Algebra k M]
  [Algebra L M]
    [IsScalarTower k L M] (c : Place k M) :
    Nat.card {σ : M ≃ₐ[L] M // SemilinearAut.ofAlgAut (σ.restrictScalars k) • c = c} =
      Nat.card ↥(c.toValuationSubring.decompositionSubgroup L)

theorem tower_bridge (w : Place K F') {T : Type*} [CommRing T] [IsDomain T]
  [IsDiscreteValuationRing T]
    [iRS : Algebra (w.restrict F).toValuationSubring w.toValuationSubring]
    [iST : Algebra w.toValuationSubring T] [iRT : Algebra (w.restrict F).toValuationSubring T]
    (hRS : iRS = (Place.restrictInclusion F w).toAlgebra)
    (hloc : IsLocalHom (algebraMap w.toValuationSubring T))
    (hinj : Function.Injective (algebraMap w.toValuationSubring T))
    (htower : ∀ r, algebraMap _ T r = algebraMap _ T (Place.restrictInclusion F w r)) :
    (maximalIdeal (w.restrict F).toValuationSubring).ramificationIdx' (maximalIdeal T) *
        (maximalIdeal T).inertiaDeg (w.restrict F).toValuationSubring =
      (w.ramificationIndex F * w.inertiaDeg F) *
        ((maximalIdeal w.toValuationSubring).ramificationIdx' (maximalIdeal T) *
          (maximalIdeal T).inertiaDeg w.toValuationSubring)

theorem ramificationIndex_mul_inertiaDeg_mul_natCard_stabilizer_eq_natCard_stabilizer
    {k F F' M : Type*} [Field k] [Field F] [Field F'] [Field M]
    [Algebra k F] [Algebra k F'] [Algebra k M] [Algebra F F'] [Algebra F M] [Algebra F' M]
    [IsScalarTower k F F'] [IsScalarTower k F M] [IsScalarTower k F' M] [IsScalarTower F F' M]
    [FiniteDimensional F F'] [FiniteDimensional F' M] [FiniteDimensional F M] [IsGalois F M]
    (c : Place k M) :
    (c.restrict F').ramificationIndex F * (c.restrict F').inertiaDeg F *
        Nat.card {σ : M ≃ₐ[F'] M // SemilinearAut.ofAlgAut (σ.restrictScalars k) • c = c} =
      Nat.card {σ : M ≃ₐ[F] M // SemilinearAut.ofAlgAut (σ.restrictScalars k) • c = c}