Module

FiniteIntermediateFieldCompositum.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FiniteIntermediateFieldCompositum

3 declarations indexed from sourceView source ↗

Module documentation

Finite intermediate-field composita

This module records the quotient cardinal and common-compositum facts for finite intermediate fields used by the norm-descent tower.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.CoreFrobeniusNorm

Imported by3

def

quotientCard

L40 ↗

ClassFormation.FiniteIntermediateField.quotientCard

Documentation

Cardinality of the finite relative Galois quotient attached to a finite intermediate field. Recording the supplied Finite instance in the definition lets later fixed-field constructions use the cardinality without adding a second finiteness parameter.

Source context 10 commands

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

universe u v
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section finiteIntermediateFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteIntermediateField

Lean source · statement

def quotientCard {E K : ClosedSubgroup G}
    (M : FiniteIntermediateField E K) : ℕ

theorem

quotientCard_pos

L48 ↗

ClassFormation.FiniteIntermediateField.quotientCard_pos

Documentation

The finite quotient used in the descent construction has positive cardinality.

Source context 10 commands

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

universe u v
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section finiteIntermediateFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteIntermediateField

Lean source · statement

theorem quotientCard_pos {E K : ClosedSubgroup G}
    (M : FiniteIntermediateField E K) : 0 < M.quotientCard

theorem

exists_common_compositum

L57 ↗

ClassFormation.FiniteIntermediateField.exists_common_compositum

Documentation

An initial finite stage and finitely many further stages have a common finite overfield. This existential form avoids choosing an artificial ordering of the finite family.

Source context 10 commands

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

universe u v
namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
open CategoryTheory
open scoped BigOperators
section finiteIntermediateFields
variable {G : Type u} [Group G] [TopologicalSpace G]
namespace FiniteIntermediateField

Lean source · statement

theorem exists_common_compositum {E K : ClosedSubgroup G} {ι : Type v}
    (M : FiniteIntermediateField E K) (s : Finset ι)
    (F : ι → FiniteIntermediateField E K) :
    ∃ P : FiniteIntermediateField E K,
      P.field.toSubgroup ≤ M.field.toSubgroup ∧
        ∀ i ∈ s, P.field.toSubgroup ≤ (F i).field.toSubgroup

Module documentation

Finite intermediate-field composita

Declarations

quotientCard

quotientCard_pos

exists_common_compositum