Module

NarrowClassGroup.lean

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.NarrowClassGroup

3 declarations indexed from sourceView source ↗

Module documentation

Narrow ideal classes

The narrow class group is the group of nonzero fractional ideals modulo principal ideals generated by elements positive at every real place. This ideal-theoretic definition does not depend on the ray class group.

Imports3

Nyll.ClassFieldTheory.Definitions.ConductorsAndRayClassFields.RayClassModulus
Nyll.ClassFieldTheory.Definitions.FrobeniusAndHilbertClassFields.NumberFieldFractionalIdealGroup
Mathlib.RingTheory.ClassGroup.Basic

Imported by2

def

totallyPositiveFieldUnits

L29 ↗

ClassFieldTheory.totallyPositiveFieldUnits

Documentation

Nonzero field elements positive at every real place.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · full declaration

def totallyPositiveFieldUnits
    (K : Type u) [Field K] [NumberField K] : Subgroup Kˣ where
  carrier := {x | ∀ v : RayClassRealPlace K,
    0 < v.1.embedding_of_isReal v.2 (x : K)}
  one_mem' := by
    intro v
    simp
  mul_mem' := by
    intro x y hx hy v
    simpa only [Units.val_mul, map_mul] using mul_pos (hx v) (hy v)
  inv_mem' := by
    intro x hx v
    simpa only [Units.val_inv_eq_inv_val, map_inv₀] using inv_pos.mpr (hx v)

def

narrowPrincipalIdealSubgroup

L44 ↗

ClassFieldTheory.narrowPrincipalIdealSubgroup

Documentation

Principal fractional ideals with a totally positive generator.

Source context 5 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace ClassFieldTheory
universe u

Lean source · statement

def narrowPrincipalIdealSubgroup
    (K : Type u) [Field K] [NumberField K] :
    Subgroup (NumberFieldFractionalIdealGroup K)

abbrev