Module

Conjugation.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.Conjugation

3 declarations indexed from sourceView source ↗

Module documentation

Hilbert ramification theory: conjugate prime ideals

This file records the conjugation statement in prime-decomposition theory: the decomposition group of a conjugate prime ideal is the conjugate subgroup.

Imports1

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.Basic

Imported by2

theorem

dedekindDecomposition_decompositionGroup_smul_eq_map_conj

L28 ↗

HilbertRamification.Dedekind.dedekindDecomposition_decompositionGroup_smul_eq_map_conj

Documentation

Decomposition and inertia groups satisfy: the decomposition group of the conjugate prime σ P is the conjugate subgroup σ G_P σ⁻¹.

Source context 5 commands

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

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

Lean source · statement

theorem dedekindDecomposition_decompositionGroup_smul_eq_map_conj
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B]
    (σ : G) :
    decompositionGroup (σ • P) G =
      (decompositionGroup P G).map (MulAut.conj σ).toMonoidHom

theorem

mem_inertiaGroup_smul_iff

L39 ↗

HilbertRamification.Dedekind.mem_inertiaGroup_smul_iff

Documentation

Prime-decomposition statement: membership in the inertia group of a conjugate prime ideal. This is the inertia-group part of the simultaneous conjugacy used later for Frobenius classes.

Source context 5 commands

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

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

Lean source · statement

theorem mem_inertiaGroup_smul_iff
    {P : Ideal B} {G : Type*} [Group G] [MulSemiringAction G B]
    {σ τ : G} :
    τ ∈ inertiaGroup (σ • P) G ↔
      σ⁻¹ * τ * σ ∈ inertiaGroup P G

theorem

dedekindRamification_inertiaGroup_smul_eq_map_conj

L62 ↗

HilbertRamification.Dedekind.dedekindRamification_inertiaGroup_smul_eq_map_conj

Documentation

Prime-decomposition statement: the inertia group of the conjugate prime σ P is the conjugate subgroup σ I_P σ⁻¹.

Source context 5 commands

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

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

Lean source · statement

theorem dedekindRamification_inertiaGroup_smul_eq_map_conj
    (P : Ideal B) (G : Type*) [Group G] [MulSemiringAction G B]
    (σ : G) :
    inertiaGroup (σ • P) G =
      (inertiaGroup P G).map (MulAut.conj σ).toMonoidHom

Module documentation

Hilbert ramification theory: conjugate prime ideals

Declarations

dedekindDecomposition_decompositionGroup_smul_eq_map_conj

mem_inertiaGroup_smul_iff

dedekindRamification_inertiaGroup_smul_eq_map_conj