Module

OrbitCardinality.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.OrbitCardinality

12 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: prime-decomposition cardinalities

This file records the parts of the prime-decomposition tower identity that are already available from the Dedekind-domain Galois action and mathlib's ramification/inertia API.

Imports1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.Basic

Imported by4

theorem

orbit_eq_singleton_of_le_stabilizer

L29 ↗

HilbertRamification.Dedekind.orbit_eq_singleton_of_le_stabilizer

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem orbit_eq_singleton_of_le_stabilizer
    {G X : Type*} [Group G] [MulAction G X]
    (H : Subgroup G) {x : X} (hH : H ≤ MulAction.stabilizer G x) :
    MulAction.orbit H x = {x}

theorem

dedekindTower_decompositionGroup_orbit_eq_singleton

L49 ↗

HilbertRamification.Dedekind.dedekindTower_decompositionGroup_orbit_eq_singleton

Documentation

The prime-decomposition tower identity: under the decomposition group G_P, the orbit of P is a singleton. This is the group-action core of the assertion that over the decomposition field Z_P, the prime P is nonsplit.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindTower_decompositionGroup_orbit_eq_singleton
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    MulAction.orbit (decompositionGroup P G) P = {P}

theorem

dedekindTower_decompositionGroup_orbit_ncard_eq_one

L58 ↗

HilbertRamification.Dedekind.dedekindTower_decompositionGroup_orbit_ncard_eq_one

Documentation

The prime-decomposition tower identity: the decomposition-group orbit of P has one element.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindTower_decompositionGroup_orbit_ncard_eq_one
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    (MulAction.orbit (decompositionGroup P G) P).ncard = 1

theorem

dedekindRamification_inertiaGroup_orbit_eq_singleton

L66 ↗

HilbertRamification.Dedekind.dedekindRamification_inertiaGroup_orbit_eq_singleton

Documentation

A prime-decomposition consequence: under the inertia group I_P, the orbit of P is a singleton.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindRamification_inertiaGroup_orbit_eq_singleton
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    MulAction.orbit (inertiaGroup P G) P = {P}

theorem

dedekindRamification_inertiaGroup_orbit_ncard_eq_one

L75 ↗

HilbertRamification.Dedekind.dedekindRamification_inertiaGroup_orbit_ncard_eq_one

Documentation

A prime-decomposition consequence: the inertia-group orbit of P has one element.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindRamification_inertiaGroup_orbit_ncard_eq_one
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    (MulAction.orbit (inertiaGroup P G) P).ncard = 1

theorem

dedekindRamification_inertiaGroup_decompositionGroup_eq_top

L84 ↗

HilbertRamification.Dedekind.dedekindRamification_inertiaGroup_decompositionGroup_eq_top

Documentation

A prime-decomposition consequence: when I_P itself is viewed as the acting Galois group, every element fixes P, so the decomposition group is the whole group.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindRamification_inertiaGroup_decompositionGroup_eq_top
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    decompositionGroup P (inertiaGroup P G) = ⊤

theorem

dedekindRamification_inertiaGroup_inertiaGroup_eq_top

L96 ↗

HilbertRamification.Dedekind.dedekindRamification_inertiaGroup_inertiaGroup_eq_top

Documentation

A prime-decomposition consequence: when I_P itself is viewed as the acting Galois group, its inertia group is the whole group.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindRamification_inertiaGroup_inertiaGroup_eq_top
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B] :
    inertiaGroup P (inertiaGroup P G) = ⊤

theorem

dedekindTower_decomposition_card_eq_ramificationIdx_mul_inertiaDeg

L109 ↗

HilbertRamification.Dedekind.dedekindTower_decomposition_card_eq_ramificationIdx_mul_inertiaDeg

Documentation

The prime-decomposition tower identity: the decomposition group has cardinality e(P/p) * f(P/p) for the chosen prime P over p, not just for the Galois-invariant representatives ramificationIdxIn and inertiaDegIn.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindTower_decomposition_card_eq_ramificationIdx_mul_inertiaDeg
    [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
    [IsTorsionFree A B]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] :
    Nat.card (decompositionGroup P G) =
      P.ramificationIdx A * P.inertiaDeg A

theorem

dedekindTower_ramificationIdxIn_mul_inertiaDegIn_eq_card_of_nonsplit

L126 ↗

HilbertRamification.Dedekind.dedekindTower_ramificationIdxIn_mul_inertiaDegIn_eq_card_of_nonsplit

Documentation

The prime-decomposition tower identity: if a prime is nonsplit in a finite Galois Dedekind extension, then the product e * f equals the order of the Galois group.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindTower_ramificationIdxIn_mul_inertiaDegIn_eq_card_of_nonsplit
    [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
    [IsTorsionFree A B]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B]
    (hnonsplit : (p.primesOver B).ncard = 1) :
    Ideal.ramificationIdxIn p B * Ideal.inertiaDegIn p B = Nat.card G

theorem

dedekindTower_ramificationIdx_mul_inertiaDeg_eq_card_of_nonsplit

L141 ↗

HilbertRamification.Dedekind.dedekindTower_ramificationIdx_mul_inertiaDeg_eq_card_of_nonsplit

Documentation

The prime-decomposition tower identity: chosen-prime form of e * f = #G under nonsplitting.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindTower_ramificationIdx_mul_inertiaDeg_eq_card_of_nonsplit
    [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
    [IsTorsionFree A B]
    (p : Ideal A) [p.IsMaximal] (hp : p ≠ ⊥)
    (P : Ideal B) [P.IsPrime] [P.LiesOver p]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B]
    (hnonsplit : (p.primesOver B).ncard = 1) :
    P.ramificationIdx A * P.inertiaDeg A =
      Nat.card G

theorem

inertia_card_eq_ramificationIdx

L160 ↗

HilbertRamification.Dedekind.inertia_card_eq_ramificationIdx

Documentation

The separable-residue cardinality relation: when the residue extension is separable, the inertia group has cardinality equal to the ramification index of the chosen prime.

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem inertia_card_eq_ramificationIdx
    [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
    [IsTorsionFree A B]
    (p : Ideal A) (P : Ideal B) [P.LiesOver p] [P.IsPrime] [P.IsMaximal]
    [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] (hp : p ≠ ⊥) :
    Nat.card (inertiaGroup P G) =
      P.ramificationIdx A

theorem

dedekindRamification_separable_residue_cardinalities

L176 ↗

HilbertRamification.Dedekind.dedekindRamification_separable_residue_cardinalities

Documentation

The separable-residue cardinality relation: the separable-residue cardinality conclusions #I_P = e(P/p) and #(G_P/I_P) = f(P/p).

Source context 6 commands

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

noncomputable section
namespace HilbertRamification
namespace Dedekind
open scoped Pointwise
open Algebra Module
variable {A B : Type*} [CommRing A] [CommRing B] [Algebra A B]

Lean source · statement

theorem dedekindRamification_separable_residue_cardinalities
    [IsDedekindDomain A] [IsDedekindDomain B] [Module.Finite A B]
    [IsTorsionFree A B]
    (p : Ideal A) [p.IsMaximal] (P : Ideal B)
    [P.IsPrime] [P.LiesOver p] [P.IsMaximal]
    [Algebra.IsSeparable (A ⧸ p) (B ⧸ P)]
    (G : Type*) [Group G] [Finite G] [MulSemiringAction G B]
    [IsGaloisGroup G A B] (hp : p ≠ ⊥) :
    Nat.card (inertiaGroup P G) =
        P.ramificationIdx A ∧
      Nat.card
          (decompositionGroup P G ⧸
            (inertiaGroup P G).subgroupOf (decompositionGroup P G)) =
        P.inertiaDeg A

Module documentation

Hilbert ramification theory: prime-decomposition cardinalities

Declarations