NYLL
Module

GaloisExtensionQuotient.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.GaloisExtensionQuotient
11 declarations indexed from sourceView source ↗

Module documentation

Finite local reciprocity: abstract extension quotients and actual Galois groups

For a Galois ambient extension Ω/K, the abstract class-formation model represents K by the closed fixing subgroup of the bottom intermediate field and an intermediate normal extension E/K by the closed subgroup fixing E. This file proves that the resulting abstract class-formation quotient is canonically the actual group Gal(E/K).

Imports2
Imported by7

Declarations

theorem

closedFixingSubgroup_bot_eq_baseField

L33 ↗
LocalClassFieldTheory.closedFixingSubgroup_bot_eq_baseField
Documentation

The subgroup fixing the bottom intermediate field is the distinguished base field of the class formation.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
theorem closedFixingSubgroup_bot_eq_baseField :
    closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω) =
      baseField (Gal(Ω / K))
theorem

fixingSubgroupLeBase

L43 ↗
LocalClassFieldTheory.fixingSubgroupLeBase
Documentation

The fixing subgroup of an intermediate field lies in the fixing subgroup of the base field.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
theorem fixingSubgroupLeBase
    (E : IntermediateField K Ω) :
    (closedFixingSubgroup K Ω E).toSubgroup ≤
      (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω)).toSubgroup
theorem

extensionSubgroup_base_eq_subgroupOf

L51 ↗
LocalClassFieldTheory.extensionSubgroup_base_eq_subgroupOf
Documentation

In the base fixing group, the abstract class-formation extension subgroup is exactly the subgroup obtained from the ambient fixing subgroup by subgroupOf.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
theorem extensionSubgroup_base_eq_subgroupOf
    (E : IntermediateField K Ω) :
    extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E) =
      (closedFixingSubgroup K Ω E).toSubgroup.subgroupOf
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω)).toSubgroup
instance

closedFixingSubgroup_normal

L62 ↗
LocalClassFieldTheory.closedFixingSubgroup_normal
Documentation

The fixing subgroup of a Galois intermediate extension is normal in the ambient Galois group.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
instance closedFixingSubgroup_normal
    (E : IntermediateField K Ω) [IsGalois K E] :
    (closedFixingSubgroup K Ω E).toSubgroup.Normal
instance

extensionSubgroupBase_normal

L69 ↗
LocalClassFieldTheory.extensionSubgroupBase_normal
Documentation

Normality of a Galois intermediate extension, in the exact subgroup presentation used by the abstract class-formation framework.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
instance extensionSubgroupBase_normal
    (E : IntermediateField K Ω) [IsGalois K E] :
    (extensionSubgroup
      (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
      (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)).Normal
def

baseFixingToAmbientQuotient

L79 ↗
LocalClassFieldTheory.baseFixingToAmbientQuotient
Documentation

The quotient map from the abstract class-formation base fixing group to the ordinary ambient quotient by Gal(Ω/E).

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
def baseFixingToAmbientQuotient
    (E : IntermediateField K Ω) [IsGalois K E] :
    (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω)).toSubgroup →*
      Gal(Ω / K) ⧸ (closedFixingSubgroup K Ω E).toSubgroup
theorem

baseFixingToAmbientQuotient_ker

L88 ↗
LocalClassFieldTheory.baseFixingToAmbientQuotient_ker
Documentation

The kernel of the preceding map is the exact extensionSubgroup used in the abstract theory.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
theorem baseFixingToAmbientQuotient_ker
    (E : IntermediateField K Ω) [IsGalois K E] :
    (baseFixingToAmbientQuotient K Ω E).ker =
      extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)
theorem

baseFixingToAmbientQuotient_surjective

L103 ↗
LocalClassFieldTheory.baseFixingToAmbientQuotient_surjective
Documentation

The base fixing group is the whole ambient Galois group, hence its map to the ambient quotient is onto.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
theorem baseFixingToAmbientQuotient_surjective
    (E : IntermediateField K Ω) [IsGalois K E] :
    Function.Surjective (baseFixingToAmbientQuotient K Ω E)
def

baseFixingExtensionQuotientEquivAmbient

L119 ↗
LocalClassFieldTheory.baseFixingExtensionQuotientEquivAmbient
Documentation

The abstract class-formation quotient for E/K is the ordinary quotient of the ambient Galois group by the subgroup fixing E.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
def baseFixingExtensionQuotientEquivAmbient
    (E : IntermediateField K Ω) [IsGalois K E] :
    ((closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω)).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)) ≃*
      Gal(Ω / K) ⧸ (closedFixingSubgroup K Ω E).toSubgroup
theorem

baseFixingExtensionQuotientEquivAmbient_mk

L134 ↗
LocalClassFieldTheory.baseFixingExtensionQuotientEquivAmbient_mk
Documentation

States the theorem baseFixingExtensionQuotientEquivAmbient_mk.

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
theorem baseFixingExtensionQuotientEquivAmbient_mk
    (E : IntermediateField K Ω) [IsGalois K E]
    (σ : (closedFixingSubgroup K Ω
      (⊥ : IntermediateField K Ω)).toSubgroup) :
    baseFixingExtensionQuotientEquivAmbient K Ω E (QuotientGroup.mk σ) =
      QuotientGroup.mk σ.1
def

baseFixingExtensionQuotientEquivGaloisGroup

L144 ↗
LocalClassFieldTheory.baseFixingExtensionQuotientEquivGaloisGroup
Documentation

The exact quotient group appearing in the abstract class-formation framework for the normal intermediate extension E/K is canonically the actual Gal(E/K).

Source context 5 commands

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

namespace LocalClassFieldTheory
open RamificationTheory CyclicCohomology
open ClassFormation
noncomputable section
variable (K Ω : Type) [Field K] [Field Ω] [Algebra K Ω] [IsGalois K Ω]
Lean source · statement
def baseFixingExtensionQuotientEquivGaloisGroup
    (E : IntermediateField K Ω) [IsGalois K E] :
    ((closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω)).toSubgroup ⧸
      extensionSubgroup
        (closedFixingSubgroup K Ω (⊥ : IntermediateField K Ω))
        (closedFixingSubgroup K Ω E) (fixingSubgroupLeBase K Ω E)) ≃*
      Gal(E / K)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.