Nyll.EtaleFundamentalGroups.Kummer.IteratedRadical.ExponentUnit.IntegralClosure

Module documentation

Exponent units from an étale normalization of an iterated radical cover

This file connects the height-two purity output to the terminal radical exponent obstruction. An integral closure inside a field is a domain and is integral over the root cover. Once purity makes it étale, those facts make it faithfully flat, so no separate chosen local factor is needed for the exponent-unit conclusion.

theorem

all_exponents_isUnit_of_iteratedRadical_integralClosure_etale

L35 ↗

EtaleFundamentalGroups.Kummer.all_exponents_isUnit_of_iteratedRadical_integralClosure_etale

Documentation

If the normalization of a positive iterated radical cover in a field is étale, and its composite with the original base is étale away from the whole boundary, then every radical exponent is a unit in the original base.

Faithful flatness of the normalization is produced internally from integrality, its domain structure, and étale flatness.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped BigOperators
universe u

Lean source · statement

theorem all_exponents_isUnit_of_iteratedRadical_integralClosure_etale
    {A : Type u} [CommRing A] [IsDomain A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (haPrime : ∀ i, Prime (a i))
    (hCharZero : ∀ i, CharZero (A ⧸ Ideal.span {a i}))
    {L : Type u} [Field L]
    [Algebra (iteratedRadical A r n a) L]
    [FaithfulSMul (iteratedRadical A r n a) L]
    (hEtale : Algebra.Etale
      (iteratedRadical A r n a)
      (integralClosure (iteratedRadical A r n a) L))
    (hAway : (Localization.awayMap
      ((algebraMap (iteratedRadical A r n a)
          (integralClosure (iteratedRadical A r n a) L)).comp
        (algebraMap A (iteratedRadical A r n a)))
      (∏ i ∈ (Finset.univ : Finset (Fin r)), a i)).Etale) :
    ∀ i, IsUnit (n i : A)

Module documentation

Exponent units from an étale normalization of an iterated radical cover

Declarations

all_exponents_isUnit_of_iteratedRadical_integralClosure_etale