Module

FiniteIntermediateCompositum.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.FiniteIntermediateCompositum

4 declarations indexed from sourceView source ↗

Module documentation

Finite intermediate fields: composita and absolute finiteness

These are the finite-stage closure facts used in the proof of the universal norm-descent lemma. The compositum of two finite intermediate fields is their intersection on the Galois-group side.

Imports1

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Construction.ReciprocityIndependence

Imported by2

def

compositum

L30 ↗

ClassFormation.FiniteIntermediateField.compositum

Documentation

The compositum of two finite intermediate fields of E / K.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace FiniteIntermediateField

Lean source · full declaration

def compositum {E K : ClosedSubgroup G}
    (M N : FiniteIntermediateField E K) :
    FiniteIntermediateField E K where
  field := M.field ⊓ N.field
  above := fun x hx => ⟨M.above hx, N.above hx⟩
  below := (inf_le_left :
    (M.field ⊓ N.field).toSubgroup ≤ M.field.toSubgroup).trans M.below
  finite := by
    let : Finite
        (K.toSubgroup ⧸ extensionSubgroup K N.field N.below) := N.finite
    exact M.compositumWith_finite_over_base N.field N.below

theorem

compositum_le_left

L43 ↗

ClassFormation.FiniteIntermediateField.compositum_le_left

Documentation

Proves the bound (M.compositum N).field.toSubgroup ≤ M.field.toSubgroup.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace FiniteIntermediateField

Lean source · statement

theorem compositum_le_left {E K : ClosedSubgroup G}
    (M N : FiniteIntermediateField E K) :
    (M.compositum N).field.toSubgroup ≤ M.field.toSubgroup

theorem

compositum_le_right

L49 ↗

ClassFormation.FiniteIntermediateField.compositum_le_right

Documentation

Proves the bound (M.compositum N).field.toSubgroup ≤ N.field.toSubgroup.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace FiniteIntermediateField

Lean source · statement

theorem compositum_le_right {E K : ClosedSubgroup G}
    (M N : FiniteIntermediateField E K) :
    (M.compositum N).field.toSubgroup ≤ N.field.toSubgroup

theorem

absoluteFinite

L56 ↗

ClassFormation.FiniteIntermediateField.absoluteFinite

Documentation

A finite intermediate field over a finite abstract base field is itself finite over the global base field.

Source context 5 commands

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

namespace ClassFormation
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G]
namespace FiniteIntermediateField

Lean source · statement

theorem absoluteFinite {E K : ClosedSubgroup G}
    [hKfinite : Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G) K (le_baseField K))]
    (M : FiniteIntermediateField E K) :
    Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G) M.field (le_baseField M.field))

Module documentation

Finite intermediate fields: composita and absolute finiteness

Declarations

compositum

compositum_le_left

compositum_le_right

absoluteFinite