ValuationSubring_exists_eq_units_mul_prod_sub_algebraMap_of_notMem_map_maximalIdeal.lean

theorem isUnit_of_isUnit_mk {S : Type*} [CommRing S] [IsLocalRing S] (I : Ideal S)
    (hI : I ≤ maximalIdeal S) (s : S) (hu : IsUnit (Ideal.Quotient.mk I s)) : IsUnit s

theorem fibre_facts {S : Type*} [CommRing S] [IsLocalRing S] (I : Ideal S) [I.IsPrime]
    (hI : I ≤ maximalIdeal S) (hnoeth : IsNoetherianRing (S ⧸ I))
    (t : S) (ht : maximalIdeal S = Ideal.span {t} ⊔ I)
    (h : S) (hh : h ∉ I) (hhu : ¬ IsUnit h) :
    ∃ n : ℕ, n ≠ 0 ∧ t ^ n ∈ Ideal.span {h} ⊔ I ∧
      (∀ P : Ideal S, P.IsPrime → I ≤ P → h ∈ P → t ∈ P) ∧
      (∀ (m : ℕ) (v h' : S), IsUnit v → m ≤ n → t ^ m * v - h * h' ∈ I → m = n ∧ IsUnit h')

theorem moduleFinite_quotient_span
    {R : Type u} [CommRing R] [HenselianLocalRing R]
    {S : Type u} [CommRing S] [IsLocalRing S] [Algebra R S] [IsLocalHom (algebraMap R S)]
    {P : Type u} [CommRing P] [Algebra R P] [Algebra.FiniteType R P] [Algebra P S] [IsScalarTower R
      P S]
    (hloc : IsLocalization ((maximalIdeal S).comap (algebraMap P S)).primeCompl S)
    (hres' : ∀ s : S, ∃ a : R, s - algebraMap R S a ∈ maximalIdeal S)
    (t : S) (ht : maximalIdeal S = Ideal.span {t} ⊔ (maximalIdeal R).map (algebraMap R S))
    (h : S) (hhmax : h ∈ maximalIdeal S)
    (hprimes : ∀ Q : Ideal S, Q.IsPrime → (maximalIdeal R).map (algebraMap R S) ≤ Q → h ∈ Q → t ∈ Q)
    (h₀ : P) (hJ : (Ideal.span {h₀}).map (algebraMap P S) = Ideal.span {h}) :
    Module.Finite R (S ⧸ Ideal.span {h})

theorem _root_.ValuationSubring.exists_eq_units_mul_prod_sub_algebraMap_of_notMem_map_maximalIdeal
    {L : Type u} [Field L] [IsAlgClosed L] (A : ValuationSubring L) [HenselianLocalRing ↥A]
    {S : Type u} [CommRing S] [IsLocalRing S] [Algebra ↥A S] [IsLocalHom (algebraMap ↥A S)]
    [Algebra.EssFiniteType ↥A S]
    (hres : Function.Surjective (algebraMap ↥A (ResidueField S)))
    (t : S) (ht : maximalIdeal S = Ideal.span {t} ⊔ (maximalIdeal ↥A).map (algebraMap ↥A S))
    (hprime : ((maximalIdeal ↥A).map (algebraMap ↥A S)).IsPrime)
    (h : S) (hh : h ∉ (maximalIdeal ↥A).map (algebraMap ↥A S)) :
    ∃ (n : ℕ) (u : Sˣ) (r : Fin n → ↥A), (∀ i, r i ∈ maximalIdeal ↥A) ∧
      h = (u : S) * ∏ i, (t - algebraMap ↥A S (r i))