Module

Iterated.lean

Nyll.EtaleFundamentalGroups.Kummer.RootCovers.Local.Iterated

3 declarations indexed from sourceView source ↗

Module documentation

Locality of finite iterated Kummer root covers

If every radicand belongs to the closed point of a local base ring, adjoining positive roots of those radicands one after another stays local. The proof also keeps track of the closed point: the image of the original maximal ideal remains inside the maximal ideal at every stage.

The resulting IsLocalRing proofs are theorems, not global recursive instances. Consumers install one proof locally when needed.

Imports2

Imported by3

theorem

exists_isLocalRing_iteratedRadical_and_map_mem_maximalIdeal

L29 ↗

EtaleFundamentalGroups.Kummer.exists_isLocalRing_iteratedRadical_and_map_mem_maximalIdeal

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem exists_isLocalRing_iteratedRadical_and_map_mem_maximalIdeal
    {A : Type u} [CommRing A] [IsLocalRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (ha : ∀ i, a i ∈ IsLocalRing.maximalIdeal A) :
    ∃ hlocal : IsLocalRing (iteratedRadical A r n a),
      ∀ x ∈ IsLocalRing.maximalIdeal A,
        algebraMap A (iteratedRadical A r n a) x ∈
          @IsLocalRing.maximalIdeal (iteratedRadical A r n a) _ hlocal

theorem

isLocalRing_iteratedRadical

L76 ↗

EtaleFundamentalGroups.Kummer.isLocalRing_iteratedRadical

Documentation

A finite iterated positive Kummer root cover of closed-point elements is local.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem isLocalRing_iteratedRadical
    {A : Type u} [CommRing A] [IsLocalRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (ha : ∀ i, a i ∈ IsLocalRing.maximalIdeal A) :
    IsLocalRing (iteratedRadical A r n a)

theorem

algebraMap_mem_maximalIdeal_iteratedRadical

L86 ↗

EtaleFundamentalGroups.Kummer.algebraMap_mem_maximalIdeal_iteratedRadical

Documentation

Under the locally supplied structure, the original closed point maps into the closed point of the finite iterated root cover.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u

Lean source · statement

theorem algebraMap_mem_maximalIdeal_iteratedRadical
    {A : Type u} [CommRing A] [IsLocalRing A]
    {r : ℕ} (n : Fin r → ℕ) (a : Fin r → A)
    (hn : ∀ i, 0 < n i)
    (ha : ∀ i, a i ∈ IsLocalRing.maximalIdeal A)
    [IsLocalRing (iteratedRadical A r n a)]
    {x : A} (hx : x ∈ IsLocalRing.maximalIdeal A) :
    algebraMap A (iteratedRadical A r n a) x ∈
      IsLocalRing.maximalIdeal (iteratedRadical A r n a)

Module documentation

Locality of finite iterated Kummer root covers

Declarations

exists_isLocalRing_iteratedRadical_and_map_mem_maximalIdeal

isLocalRing_iteratedRadical

algebraMap_mem_maximalIdeal_iteratedRadical