EtaleFundamentalGroups.Kummer.all_exponents_isUnit_of_formallyUnramified_boundaryIteratedRadical
Every exponent of a formally unramified iterated Kummer radical on a full prime-boundary complement is already a unit in the original domain.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped BigOperators
universe u vLean source · full declaration
theorem all_exponents_isUnit_of_formallyUnramified_boundaryIteratedRadical
{R : Type u} {S : Type v} [CommRing R] [IsDomain R]
[CommRing S] [Algebra R S]
{r : ℕ} (t : Fin r → R)
[IsLocalization.Away
(∏ i ∈ (Finset.univ : Finset (Fin r)), t i) S]
(ht : ∀ i, Prime (t i))
(hCharZero : ∀ i, CharZero (R ⧸ Ideal.span {t i}))
(n : Fin r → ℕ) (hn : ∀ i, 0 < n i)
[Algebra.FormallyUnramified S
(iteratedRadical S r n (fun i ↦ algebraMap R S (t i)))] :
∀ i, IsUnit (n i : R) := by
have hBoundary_ne :
(∏ i ∈ (Finset.univ : Finset (Fin r)), t i) ≠ 0 :=
Finset.prod_ne_zero_iff.mpr fun i _ ↦ (ht i).ne_zero
let : IsDomain S :=
IsLocalization.Away.isDomain S hBoundary_ne
have hnS : ∀ i, IsUnit (n i : S) :=
all_exponents_isUnit_of_formallyUnramified_iteratedRadical
(A := S) n (fun i ↦ algebraMap R S (t i)) hn
intro i
exact
isUnit_natCast_of_isUnit_algebraMap_away_finsetProduct
(R := R) (S := S) Finset.univ t
(fun j _ ↦ ht j) (fun j _ ↦ hCharZero j) (hn i) (by
simpa using hnS i)