Module

LocalDerivative.lean

Nyll.EtaleFundamentalGroups.Kummer.Obstructions.LocalDerivative

5 declarations indexed from sourceView source ↗

Module documentation

Eisenstein irreducibility for an explicit Kummer polynomial

For a prime element t, the polynomial X ^ n - t is Eisenstein at (t). If the original domain is integrally closed, Gauss's lemma then transports this irreducibility to its fraction field. This is the field shared by the original domain and its boundary localization, where the Kummer cover is etale.

Imports4

Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Mathlib.RingTheory.Polynomial.GaussLemma
Mathlib.RingTheory.Localization.AsSubring
Mathlib.RingTheory.Localization.Away.Basic

Imported by6

theorem

prime_notMem_span_singleton_sq

L29 ↗

EtaleFundamentalGroups.Kummer.prime_notMem_span_singleton_sq

Documentation

A prime element does not belong to the square of its principal ideal.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v

Lean source · statement

theorem prime_notMem_span_singleton_sq
    {R : Type u} [CommRing R] [IsDomain R] {t : R} (ht : Prime t) :
    t ∉ (Ideal.span ({t} : Set R)) ^ 2

theorem

isEisensteinAt_X_pow_sub_C_of_prime

L42 ↗

EtaleFundamentalGroups.Kummer.isEisensteinAt_X_pow_sub_C_of_prime

Documentation

X ^ n - t is Eisenstein at (t) when t is prime and n is positive.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v

Lean source · statement

theorem isEisensteinAt_X_pow_sub_C_of_prime
    {R : Type u} [CommRing R] [IsDomain R] {t : R} (ht : Prime t)
    {n : ℕ} (hn : 0 < n) :
    (X ^ n - C t).IsEisensteinAt (Ideal.span ({t} : Set R))

theorem

irreducible_X_pow_sub_C_of_prime

L60 ↗

EtaleFundamentalGroups.Kummer.irreducible_X_pow_sub_C_of_prime

Documentation

X ^ n - t is irreducible when t is prime and n is positive.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v

Lean source · statement

theorem irreducible_X_pow_sub_C_of_prime
    {R : Type u} [CommRing R] [IsDomain R] {t : R} (ht : Prime t)
    {n : ℕ} (hn : 0 < n) :
    Irreducible (X ^ n - C t)

theorem

irreducible_X_pow_sub_C_fractionRing_of_prime

L74 ↗

EtaleFundamentalGroups.Kummer.irreducible_X_pow_sub_C_fractionRing_of_prime

Documentation

The explicit Kummer polynomial remains irreducible over any chosen fraction field of an integrally closed original domain. The only coefficient map in the statement is the canonical algebraMap R K.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v

Lean source · statement

theorem irreducible_X_pow_sub_C_fractionRing_of_prime
    {R : Type u} {K : Type v} [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [Field K] [Algebra R K] [IsFractionRing R K] {t : R} (ht : Prime t)
    {n : ℕ} (hn : 0 < n) :
    Irreducible (X ^ n - C (algebraMap R K t))

theorem

irreducible_X_pow_sub_C_away_of_prime

L90 ↗

EtaleFundamentalGroups.Kummer.irreducible_X_pow_sub_C_away_of_prime

Documentation

After inverting the boundary parameter, the same Kummer polynomial remains irreducible. The proof uses the single canonical map from the localization to the chosen fraction field; it does not introduce an algebra tower.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Kummer
open Polynomial
universe u v

Lean source · statement

theorem irreducible_X_pow_sub_C_away_of_prime
    {R : Type u} {S : Type v} {K : Type*}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing S] [Algebra R S] {t : R} [IsLocalization.Away t S]
    [Field K] [Algebra R K] [IsFractionRing R K] (ht : Prime t)
    {n : ℕ} (hn : 0 < n) :
    Irreducible (X ^ n - C (algebraMap R S t))

Module documentation

Eisenstein irreducibility for an explicit Kummer polynomial

Declarations

prime_notMem_span_singleton_sq

isEisensteinAt_X_pow_sub_C_of_prime

irreducible_X_pow_sub_C_of_prime

irreducible_X_pow_sub_C_fractionRing_of_prime

irreducible_X_pow_sub_C_away_of_prime