Module

Basic.lean

Nyll.EtaleFundamentalGroups.Kummer.RootCovers.Local.Basic

4 declarations indexed from sourceView source ↗

Module documentation

Local Kummer root covers

This file identifies the closed point of the one-step root cover R[X] / (X ^ n - a) when R is local and a lies in its maximal ideal.

Imports5

Nyll.EtaleFundamentalGroups.Kummer.Radicals.Explicit
Mathlib.RingTheory.Ideal.GoingUp
Mathlib.RingTheory.LocalRing.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by5

def

localRootCoverClosedIdeal

L32 ↗

EtaleFundamentalGroups.Kummer.localRootCoverClosedIdeal

Documentation

The closed-point ideal in the one-step root cover R[X] / (X ^ n - a): it is generated by the image of the maximal ideal of R and the adjoined root.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
noncomputable section

Lean source · statement

def localRootCoverClosedIdeal
    (R : Type u) [CommRing R] [IsLocalRing R] (n : ℕ) (a : R) :
    Ideal (AdjoinRoot (X ^ n - C a))

theorem

localRootCoverClosedIdeal_isMaximal

L42 ↗

EtaleFundamentalGroups.Kummer.localRootCoverClosedIdeal_isMaximal

Documentation

If a belongs to the closed point of a local ring and n is positive, the explicit closed-point ideal of R[X] / (X ^ n - a) is maximal.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
noncomputable section

Lean source · statement

theorem localRootCoverClosedIdeal_isMaximal
    {R : Type u} [CommRing R] [IsLocalRing R] {n : ℕ} (hn : 0 < n)
    {a : R} (ha : a ∈ IsLocalRing.maximalIdeal R) :
    (localRootCoverClosedIdeal R n a).IsMaximal

theorem

isLocalRing_adjoinRoot_X_pow_sub_C

L118 ↗

EtaleFundamentalGroups.Kummer.isLocalRing_adjoinRoot_X_pow_sub_C

Documentation

The positive one-step root cover of a closed-point element of a local ring is again a local ring. This is a theorem rather than a global instance so that consumers can install it only in the proof scope where it is needed.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
noncomputable section

Lean source · statement

theorem isLocalRing_adjoinRoot_X_pow_sub_C
    {R : Type u} [CommRing R] [IsLocalRing R] {n : ℕ} (hn : 0 < n)
    {a : R} (ha : a ∈ IsLocalRing.maximalIdeal R) :
    IsLocalRing (AdjoinRoot (X ^ n - C a))

theorem

maximalIdeal_adjoinRoot_X_pow_sub_C

L160 ↗

EtaleFundamentalGroups.Kummer.maximalIdeal_adjoinRoot_X_pow_sub_C

Documentation

The unique maximal ideal of the local root cover is the image of the base maximal ideal together with the adjoined root.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u
noncomputable section

Lean source · statement

theorem maximalIdeal_adjoinRoot_X_pow_sub_C
    {R : Type u} [CommRing R] [IsLocalRing R] {n : ℕ} (hn : 0 < n)
    {a : R} (ha : a ∈ IsLocalRing.maximalIdeal R)
    [IsLocalRing (AdjoinRoot (X ^ n - C a))] :
    IsLocalRing.maximalIdeal (AdjoinRoot (X ^ n - C a)) =
      localRootCoverClosedIdeal R n a

Module documentation

Local Kummer root covers

Declarations

localRootCoverClosedIdeal

localRootCoverClosedIdeal_isMaximal

isLocalRing_adjoinRoot_X_pow_sub_C

maximalIdeal_adjoinRoot_X_pow_sub_C