EtaleFundamentalGroups.Kummer.exponent_isUnit_of_oneRoot_samePrime_completion
A literal finite-etale factor over the one-root cover forces the root exponent to be a unit in the original two-dimensional base.
All completion geometry is produced from the prime parameter and regularity of its quotient. The same closed prime p is retained through the faithfully-flat Henselian pushout by the imported same-prime theorem.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open IsLocalRing
universe uA uELean source · full declaration
theorem exponent_isUnit_of_oneRoot_samePrime_completion
{A : Type uA} [CommRing A] [IsDomain A] [IsRegularLocalRing A]
{N : ℕ} (hN : 0 < N) {y : A} (hy : Prime y)
(hyQuot : IsRegularLocalRing (A ⧸ Ideal.span ({y} : Set A)))
(hdim : ringKrullDim A = ((2 : ℕ∞) : WithBot ℕ∞))
(hCharZero : CharZero (A ⧸ Ideal.span ({y} : Set A)))
{E : Type uE} [CommRing E]
[Algebra
(iteratedRadical A 1 (fun _ : Fin 1 ↦ N) (fun _ : Fin 1 ↦ y)) E]
[Algebra A E]
[IsScalarTower A
(iteratedRadical A 1 (fun _ : Fin 1 ↦ N) (fun _ : Fin 1 ↦ y)) E]
[Module.Finite
(iteratedRadical A 1 (fun _ : Fin 1 ↦ N) (fun _ : Fin 1 ↦ y)) E]
[Algebra.Etale
(iteratedRadical A 1 (fun _ : Fin 1 ↦ N) (fun _ : Fin 1 ↦ y)) E]
(p : Ideal E) [p.IsMaximal]
[hpOver :
letI : IsLocalRing
(iteratedRadical A 1
(fun _ : Fin 1 ↦ N) (fun _ : Fin 1 ↦ y)) :=
isLocalRing_iteratedRadical
(fun _ : Fin 1 ↦ N) (fun _ : Fin 1 ↦ y)
(fun _ ↦ hN) (fun _ ↦ by
rw [mem_maximalIdeal]
exact hy.not_isUnit)
p.LiesOver
(maximalIdeal
(iteratedRadical A 1
(fun _ : Fin 1 ↦ N) (fun _ : Fin 1 ↦ y)))]
(hAway :
(Localization.awayMap
(algebraMap A (Localization.AtPrime p)) y).Etale) :
IsUnit (N : A) := by
obtain ⟨z, hreg, hgen⟩ :=
exists_regular_pair_of_prime_regular_quotient_dimension_two
hy hyQuot hdim
let n : Fin 1 → ℕ := fun _ ↦ N
let a : Fin 1 → A := fun _ ↦ y
let s : Fin 1 → A := fun _ ↦ y
have hn : ∀ i, 0 < n i := by
intro i
simpa [n] using hN
have hstage : ∀ i, a i ∈ maximalIdeal A ∨ n i = 1 := by
intro i
left
rw [mem_maximalIdeal]
simpa [a] using hy.not_isUnit
let : IsLocalRing (iteratedRadical A 1 n a) :=
isLocalRing_iteratedRadical_of_mem_or_eq_one n a hn hstage
have hsPrimeOrUnit : ∀ i, Prime (s i) ∨ IsUnit (s i) := by
intro i
exact Or.inl (by simpa [s] using hy)
have hCharZeroS : ∀ i, Prime (s i) →
CharZero (A ⧸ Ideal.span {s i}) := by
intro i _
simpa [s] using hCharZero
have hAssoc : Associated y (∏ i, s i) := by
simp [s]
have hcompletion :=
maximalAdicCompletion_regularPair_geometry hreg hgen
have hall :=
all_exponents_isUnit_of_conditionalIteratedRadical_samePrime_completion
(A := A) n a hn hstage s hsPrimeOrUnit hCharZeroS
y hAssoc hcompletion.1
(maximalAdicCompletion_isNoetherianRing_of_regularPair hreg hgen)
(fun i _ ↦ by simpa [s] using hcompletion.2.2.2.1)
(E := E) p hAway
simpa [n] using hall (0 : Fin 1)