NYLL
Module

Reduction.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.Reduction
36 declarations indexed from sourceView source ↗

Module documentation

The abstract reciprocity theorem: actual reduction maps

This file isolates the field- and quotient-theoretic content of the three reductions. In particular, the Sylow reduction uses an intermediate field which need not be normal over the base. We therefore construct its norm map without a normality assumption on the intermediate extension.

The reciprocity homomorphisms themselves belong to the finite reciprocity equivalence. The lemmas below only construct the actual arrows and prove the algebraic diagram chases which will be applied to those homomorphisms.

The maximal unramified subextension in the third reduction

Imports3
Imported by7

Declarations

def

intermediateNormMap

L50 ↗
ClassFormation.FiniteGaloisSubextension.intermediateNormMap
Documentation

The norm arrow A_M / N_{L/M} A_L → A_K / N_{L/K} A_L for the actual intermediate field cut out by S ≤ G(L/K). No normality of M/K is used.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · full declaration
def intermediateNormMap (A : Rep ℤ G) (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    let M := L.intermediateField S
    let hLM := L.field_le_intermediateField S
    letI : Finite (M.toSubgroup ⧸ extensionSubgroup M L.field hLM) :=
      L.extension_over_intermediate_finite S
    letI : Finite (K.toSubgroup ⧸ extensionSubgroup K L.field L.below) :=
      L.finite
    FiniteNormQuotient A M L.field hLM →+
      FiniteNormQuotient A K L.field L.below := by
  let M := L.intermediateField S
  let hLM := L.field_le_intermediateField S
  let hMK := L.intermediateField_le_base S
  letI : Finite (K.toSubgroup ⧸
      extensionSubgroup K L.field L.below) := L.finite
  letI : Finite (M.toSubgroup ⧸
      extensionSubgroup M L.field hLM) :=
    L.extension_over_intermediate_finite S
  letI : Finite (K.toSubgroup ⧸ extensionSubgroup K M hMK) :=
    L.intermediateField_finite S
  exact finiteReciprocityNaturalityNormMap A K M L.field L.field
    L.below hLM hMK le_rfl
theorem

intermediateNormMap_finiteNormClass

L75 ↗
ClassFormation.FiniteGaloisSubextension.intermediateNormMap_finiteNormClass
Documentation

Representative formula for the nonnormal-intermediate norm arrow.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · full declaration
theorem intermediateNormMap_finiteNormClass (A : Rep ℤ G)
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient)
    (a : ambientFixedAddSubgroup A (L.intermediateField S)) :
    letI : Finite (K.toSubgroup ⧸
        extensionSubgroup K L.field L.below) := L.finite
    letI : Finite ((L.intermediateField S).toSubgroup ⧸
        extensionSubgroup (L.intermediateField S) L.field
          (L.field_le_intermediateField S)) :=
      L.extension_over_intermediate_finite S
    letI : Finite (K.toSubgroup ⧸ extensionSubgroup K
        (L.intermediateField S) (L.intermediateField_le_base S)) :=
      L.intermediateField_finite S
    L.intermediateNormMap A S
        (finiteNormClass A (L.intermediateField S) L.field
          (L.field_le_intermediateField S) a) =
      finiteNormClass A K L.field L.below
        (relativeNorm A K (L.intermediateField S)
          (L.intermediateField_le_base S) a) := by
  let : Finite (K.toSubgroup ⧸
      extensionSubgroup K L.field L.below) := L.finite
  let : Finite ((L.intermediateField S).toSubgroup ⧸
      extensionSubgroup (L.intermediateField S) L.field
        (L.field_le_intermediateField S)) :=
    L.extension_over_intermediate_finite S
  let : Finite (K.toSubgroup ⧸ extensionSubgroup K
      (L.intermediateField S) (L.intermediateField_le_base S)) :=
    L.intermediateField_finite S
  exact finiteReciprocityNaturalityNormMap_finiteNormClass A K
    (L.intermediateField S) L.field L.field L.below
    (L.field_le_intermediateField S) (L.intermediateField_le_base S) le_rfl a
def

intermediateNormQuotientInclusion

L108 ↗
ClassFormation.FiniteGaloisSubextension.intermediateNormQuotientInclusion
Documentation

Inclusion of fixed elements, descended to the two actual norm quotients. This is the map i in the Sylow argument.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · full declaration
def intermediateNormQuotientInclusion (A : Rep ℤ G)
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    letI : Finite (K.toSubgroup ⧸
        extensionSubgroup K L.field L.below) := L.finite
    letI : Finite ((L.intermediateField S).toSubgroup ⧸
        extensionSubgroup (L.intermediateField S) L.field
          (L.field_le_intermediateField S)) :=
      L.extension_over_intermediate_finite S
    FiniteNormQuotient A K L.field L.below →+
      FiniteNormQuotient A (L.intermediateField S) L.field
        (L.field_le_intermediateField S) := by
  letI : Finite (K.toSubgroup ⧸
      extensionSubgroup K L.field L.below) := L.finite
  letI : (extensionSubgroup K L.field L.below).Normal := L.normal
  letI : (extensionSubgroup (L.intermediateField S) L.field
      (L.field_le_intermediateField S)).Normal :=
    L.extensionSubgroup_over_intermediate_normal S
  letI : Finite ((L.intermediateField S).toSubgroup ⧸
      extensionSubgroup (L.intermediateField S) L.field
        (L.field_le_intermediateField S)) :=
    L.extension_over_intermediate_finite S
  exact transferNormNaturalityNormQuotientInclusion A K (L.intermediateField S)
    L.field (L.field_le_intermediateField S)
      (L.intermediateField_le_base S)
theorem

intermediateNormQuotientInclusion_finiteNormClass

L136 ↗
ClassFormation.FiniteGaloisSubextension.intermediateNormQuotientInclusion_finiteNormClass
Documentation

Representative formula for the inclusion used in the Sylow reduction.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · full declaration
theorem intermediateNormQuotientInclusion_finiteNormClass (A : Rep ℤ G)
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient)
    (a : ambientFixedAddSubgroup A K) :
    letI : Finite (K.toSubgroup ⧸
        extensionSubgroup K L.field L.below) := L.finite
    letI : Finite ((L.intermediateField S).toSubgroup ⧸
        extensionSubgroup (L.intermediateField S) L.field
          (L.field_le_intermediateField S)) :=
      L.extension_over_intermediate_finite S
    L.intermediateNormQuotientInclusion A S
        (finiteNormClass A K L.field L.below a) =
      finiteNormClass A (L.intermediateField S) L.field
        (L.field_le_intermediateField S)
        (fixedFieldInclusion A K (L.intermediateField S)
          (L.intermediateField_le_base S) a) := by
  let : Finite (K.toSubgroup ⧸
      extensionSubgroup K L.field L.below) := L.finite
  let : (extensionSubgroup K L.field L.below).Normal := L.normal
  let : (extensionSubgroup (L.intermediateField S) L.field
      (L.field_le_intermediateField S)).Normal :=
    L.extensionSubgroup_over_intermediate_normal S
  let : Finite ((L.intermediateField S).toSubgroup ⧸
      extensionSubgroup (L.intermediateField S) L.field
        (L.field_le_intermediateField S)) :=
    L.extension_over_intermediate_finite S
  exact transferNormNaturality_normQuotientInclusion_finiteNormClass A K
    (L.intermediateField S) L.field (L.field_le_intermediateField S)
      (L.intermediateField_le_base S) a
theorem

intermediateNormMap_comp_inclusion

L167 ↗
ClassFormation.FiniteGaloisSubextension.intermediateNormMap_comp_inclusion
Documentation

The exact identity N_{M/K} ∘ i = [M:K], now for an arbitrary (possibly nonnormal) intermediate field.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · full declaration
theorem intermediateNormMap_comp_inclusion (A : Rep ℤ G)
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    letI : Finite (K.toSubgroup ⧸
        extensionSubgroup K L.field L.below) := L.finite
    ∀ q : FiniteNormQuotient A K L.field L.below,
    letI : Finite ((L.intermediateField S).toSubgroup ⧸
        extensionSubgroup (L.intermediateField S) L.field
          (L.field_le_intermediateField S)) :=
      L.extension_over_intermediate_finite S
    letI : Finite (K.toSubgroup ⧸ extensionSubgroup K
        (L.intermediateField S) (L.intermediateField_le_base S)) :=
      L.intermediateField_finite S
    L.intermediateNormMap A S
        (L.intermediateNormQuotientInclusion A S q) =
      ((L.intermediateFiniteAbstractExtension S).degree : ℕ) • q := by
  let : Finite (K.toSubgroup ⧸
      extensionSubgroup K L.field L.below) := L.finite
  intro q
  let : (extensionSubgroup K L.field L.below).Normal := L.normal
  let : (extensionSubgroup (L.intermediateField S) L.field
      (L.field_le_intermediateField S)).Normal :=
    L.extensionSubgroup_over_intermediate_normal S
  let : Finite ((L.intermediateField S).toSubgroup ⧸
      extensionSubgroup (L.intermediateField S) L.field
        (L.field_le_intermediateField S)) :=
    L.extension_over_intermediate_finite S
  let : Finite (K.toSubgroup ⧸ extensionSubgroup K
      (L.intermediateField S) (L.intermediateField_le_base S)) :=
    L.intermediateField_finite S
  refine FiniteNormQuotient.induction_on A K L.field L.below q ?_
  intro a
  rw [intermediateNormQuotientInclusion_finiteNormClass,
    intermediateNormMap_finiteNormClass]
  rw [show relativeNorm A K (L.intermediateField S)
      (L.intermediateField_le_base S)
        (fixedFieldInclusion A K (L.intermediateField S)
          (L.intermediateField_le_base S) a) =
      ((L.intermediateFiniteAbstractExtension S).degree : ℕ) • a by
    change relativeNorm A
        (L.intermediateFiniteAbstractExtension S).base
        (L.intermediateFiniteAbstractExtension S).field
        (L.intermediateFiniteAbstractExtension S).below
        (fixedFieldInclusion A
          (L.intermediateFiniteAbstractExtension S).base
          (L.intermediateFiniteAbstractExtension S).field
          (L.intermediateFiniteAbstractExtension S).below a) =
      ((L.intermediateFiniteAbstractExtension S).degree : ℕ) • a
    exact relativeNorm_fixedFieldInclusion A
      (L.intermediateFiniteAbstractExtension S) a]
  exact finiteNormClass_nsmul A K L.field L.below _ a
def

lowerInclusionHom

L232 ↗
ClassFormation.FiniteGaloisSubextension.lowerInclusionHom
Documentation

The inclusion G(L/M) → G(L/K) for the actual intermediate field, obtained from G(L/M) ≃ S followed by the subgroup inclusion.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
def lowerInclusionHom (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    (L.intermediateField S).toSubgroup ⧸
        extensionSubgroup (L.intermediateField S) L.field
          (L.field_le_intermediateField S) →*
      L.extensionQuotient
theorem

lowerInclusionHom_mk

L242 ↗
ClassFormation.FiniteGaloisSubextension.lowerInclusionHom_mk
Documentation

Representative formula for the actual lower inclusion.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem lowerInclusionHom_mk (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient)
    (m : (L.intermediateField S).toSubgroup) :
    L.lowerInclusionHom S (QuotientGroup.mk m) =
      (QuotientGroup.mk'
        (extensionSubgroup K L.field L.below))
          ⟨m.1, L.intermediateField_le_base S m.property⟩
theorem

lowerInclusionHom_injective

L252 ↗
ClassFormation.FiniteGaloisSubextension.lowerInclusionHom_injective
Documentation

The lower inclusion is injective.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem lowerInclusionHom_injective (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    Function.Injective (L.lowerInclusionHom S)
theorem

lowerQuotient_isCyclic

L260 ↗
ClassFormation.FiniteGaloisSubextension.lowerQuotient_isCyclic
Documentation

Every lower quotient of a cyclic extension is cyclic.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem lowerQuotient_isCyclic (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [IsCyclic L.extensionQuotient] :
    IsCyclic
      ((L.intermediateField S).toSubgroup ⧸
        extensionSubgroup (L.intermediateField S) L.field
          (L.field_le_intermediateField S))
def

upperRestrictionHom

L271 ↗
ClassFormation.FiniteGaloisSubextension.upperRestrictionHom
Documentation

The actual restriction arrow G(L/K) → G(M/K) attached to a normal subgroup S ◁ G(L/K), expressed through the third-isomorphism identification constructed in IntermediateExtension.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
def upperRestrictionHom (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] :
    L.extensionQuotient →*
      K.toSubgroup ⧸ extensionSubgroup K (L.intermediateField S)
        (L.intermediateField_le_base S)
theorem

upperRestrictionHom_mk

L280 ↗
ClassFormation.FiniteGaloisSubextension.upperRestrictionHom_mk
Documentation

Representative formula for the actual upper restriction arrow.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem upperRestrictionHom_mk (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] (k : K.toSubgroup) :
    L.upperRestrictionHom S
        (QuotientGroup.mk k : L.extensionQuotient) =
      QuotientGroup.mk k
theorem

upperRestrictionHom_surjective

L288 ↗
ClassFormation.FiniteGaloisSubextension.upperRestrictionHom_surjective
Documentation

Restriction to a normal intermediate field is surjective.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem upperRestrictionHom_surjective (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] :
    Function.Surjective (L.upperRestrictionHom S)
theorem

upperQuotient_isCyclic

L295 ↗
ClassFormation.FiniteGaloisSubextension.upperQuotient_isCyclic
Documentation

Every upper quotient of a cyclic extension is cyclic.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem upperQuotient_isCyclic (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal]
    [IsCyclic L.extensionQuotient] :
    IsCyclic
      (K.toSubgroup ⧸ extensionSubgroup K (L.intermediateField S)
        (L.intermediateField_le_base S))
theorem

upperRestrictionHom_eq_one_iff

L307 ↗
ClassFormation.FiniteGaloisSubextension.upperRestrictionHom_eq_one_iff
Documentation

Its kernel is exactly the subgroup defining the intermediate field.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem upperRestrictionHom_eq_one_iff (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal]
    (q : L.extensionQuotient) :
    L.upperRestrictionHom S q = 1 ↔ q ∈ S
theorem

intermediateGalois_exact

L328 ↗
ClassFormation.FiniteGaloisSubextension.intermediateGalois_exact
Documentation

Exactness of the actual upper row for an intermediate field, in additive form for direct use with the reciprocity homomorphisms.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem intermediateGalois_exact (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] :
    Function.Exact
      (MonoidHom.toAdditive (L.lowerInclusionHom S))
      (MonoidHom.toAdditive (L.upperRestrictionHom S))
def

abelianIntermediateField

L357 ↗
ClassFormation.FiniteGaloisSubextension.abelianIntermediateField
Documentation

The maximal abelian intermediate field in the first reduction is the actual field cut out by the commutator subgroup of G(L/K).

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
def abelianIntermediateField (L : FiniteGaloisSubextension K) :
    ClosedSubgroup G
instance

abelianIntermediateField_normalInstance

L362 ↗
ClassFormation.FiniteGaloisSubextension.abelianIntermediateField_normalInstance
Documentation

Normality of the maximal abelian intermediate extension.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
instance abelianIntermediateField_normalInstance
    (L : FiniteGaloisSubextension K) :
    (extensionSubgroup K L.abelianIntermediateField
      (L.intermediateField_le_base
        (commutator L.extensionQuotient))).Normal
def

abelianRestrictionHom

L375 ↗
ClassFormation.FiniteGaloisSubextension.abelianRestrictionHom
Documentation

Restriction to the maximal abelian intermediate field.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
def abelianRestrictionHom (L : FiniteGaloisSubextension K) :
    L.extensionQuotient →*
      K.toSubgroup ⧸ extensionSubgroup K L.abelianIntermediateField
        (L.intermediateField_le_base
          (commutator L.extensionQuotient))
theorem

abelianRestrictionHom_eq_one_iff

L384 ↗
ClassFormation.FiniteGaloisSubextension.abelianRestrictionHom_eq_one_iff
Documentation

The first reduction's exact upper-row assertion: the kernel of restriction to L^ab is the commutator subgroup.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem abelianRestrictionHom_eq_one_iff
    (L : FiniteGaloisSubextension K) (q : L.extensionQuotient) :
    L.abelianRestrictionHom q = 1 ↔
      q ∈ commutator L.extensionQuotient
theorem

upperRestrictionHom_jointlyFaithful

L393 ↗
ClassFormation.FiniteGaloisSubextension.upperRestrictionHom_jointlyFaithful
Documentation

A jointly faithful family of quotient coordinates gives a jointly faithful family of actual restriction maps to the corresponding intermediate fields.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem upperRestrictionHom_jointlyFaithful
    (L : FiniteGaloisSubextension K)
    {I : Type*} {C : I → Type*} [∀ i, Group (C i)]
    (f : ∀ i, L.extensionQuotient →* C i)
    (hfaithful : (⨅ i, MonoidHom.ker (f i)) = ⊥)
    (q : L.extensionQuotient) :
    (∀ i, L.upperRestrictionHom (MonoidHom.ker (f i)) q = 1) ↔
      q = 1
theorem

upperRestrictionHom_ker_factor

L416 ↗
ClassFormation.FiniteGaloisSubextension.upperRestrictionHom_ker_factor
Documentation

For a coordinate homomorphism, the actual restriction map has exactly the same kernel.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem upperRestrictionHom_ker_factor
    (L : FiniteGaloisSubextension K) {C : Type*} [Group C]
    (f : L.extensionQuotient →* C) (q : L.extensionQuotient) :
    L.upperRestrictionHom (MonoidHom.ker f) q = 1 ↔ f q = 1
theorem

exists_cyclicIntermediateFields

L427 ↗
ClassFormation.FiniteGaloisSubextension.exists_cyclicIntermediateFields
Documentation

A finite abelian G(L/K) supplies the actual cyclic intermediate extensions used in the second reduction. The coordinate kernels have trivial intersection, and the corresponding groups G(Mᵢ/K) are finite cyclic.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem exists_cyclicIntermediateFields
    (L : FiniteGaloisSubextension K)
    [IsMulCommutative L.extensionQuotient] :
    ∃ (I : Type 0) (_ : Fintype I) (m : I → ℕ),
      (∀ i, 1 < m i) ∧
      ∃ f : ∀ i,
          L.extensionQuotient →* Multiplicative (ZMod (m i)),
        (∀ i, Function.Surjective (f i)) ∧
        (⨅ i, MonoidHom.ker (f i)) = ⊥ ∧
        (∀ i, IsCyclic
          (K.toSubgroup ⧸ extensionSubgroup K
            (L.intermediateField (MonoidHom.ker (f i)))
            (L.intermediateField_le_base (MonoidHom.ker (f i))))) ∧
        (∀ i, Finite
          (K.toSubgroup ⧸ extensionSubgroup K
            (L.intermediateField (MonoidHom.ker (f i)))
            (L.intermediateField_le_base (MonoidHom.ker (f i)))))
def

inertiaImage

L466 ↗
ClassFormation.FiniteGaloisSubextension.inertiaImage
Documentation

The inertia subgroup of G(L/K): the image of I_K in the actual finite quotient. Its fixed field is L ∩ K̃ in the notation of.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
def inertiaImage (D : DegreeData G) (L : FiniteGaloisSubextension K) :
    Subgroup L.extensionQuotient
theorem

inertiaImage_normal

L474 ↗
ClassFormation.FiniteGaloisSubextension.inertiaImage_normal
Documentation

The inertia image is normal, since it is the image of the normal inertia subgroup under a surjective quotient map.

Source context 10 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in
Lean source · statement
theorem inertiaImage_normal (D : DegreeData G)
    (L : FiniteGaloisSubextension K) : (L.inertiaImage D).Normal
instance

inertiaImage_normalInstance

L482 ↗
ClassFormation.FiniteGaloisSubextension.inertiaImage_normalInstance
Documentation

The inertia image in a finite Galois quotient is normal.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
instance inertiaImage_normalInstance (D : DegreeData G)
    (L : FiniteGaloisSubextension K) : (L.inertiaImage D).Normal
def

maximalUnramifiedSubextension

L487 ↗
ClassFormation.FiniteGaloisSubextension.maximalUnramifiedSubextension
Documentation

The actual maximal unramified subextension M = L ∩ K̃.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
def maximalUnramifiedSubextension (D : DegreeData G)
    (L : FiniteGaloisSubextension K) : ClosedSubgroup G
def

maximalUnramifiedFiniteGalois

L492 ↗
ClassFormation.FiniteGaloisSubextension.maximalUnramifiedFiniteGalois
Documentation

M/K as an actual finite Galois extension.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
def maximalUnramifiedFiniteGalois (D : DegreeData G)
    (L : FiniteGaloisSubextension K) : FiniteGaloisSubextension K
theorem

maximalUnramifiedSubextension_isUnramified

L498 ↗
ClassFormation.FiniteGaloisSubextension.maximalUnramifiedSubextension_isUnramified
Documentation

The constructed M/K is unramified.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem maximalUnramifiedSubextension_isUnramified
    (D : DegreeData G) (L : FiniteGaloisSubextension K) :
    (DegreeData.AbstractExtension.mk (L.maximalUnramifiedSubextension D) K
      (L.intermediateField_le_base (L.inertiaImage D))).IsUnramified D
theorem

maximalUnramifiedSubextension_isTotallyRamified

L524 ↗
ClassFormation.FiniteGaloisSubextension.maximalUnramifiedSubextension_isTotallyRamified
Documentation

The complementary extension L/M is totally ramified, i.e. f_{L/M}=1.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem maximalUnramifiedSubextension_isTotallyRamified
    (D : DegreeData G) (L : FiniteGaloisSubextension K) :
    (DegreeData.AbstractExtension.mk L.field
      (L.maximalUnramifiedSubextension D)
      (L.field_le_intermediateField (L.inertiaImage D))).IsTotallyRamified D
theorem

maximalUnramifiedSubextension_le_of_isUnramified

L560 ↗
ClassFormation.FiniteGaloisSubextension.maximalUnramifiedSubextension_le_of_isUnramified
Documentation

Maximality: every unramified intermediate extension of L/K is contained in the field cut out by the inertia image. In subgroup order this is the displayed inclusion.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section GroupOnly
variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · statement
theorem maximalUnramifiedSubextension_le_of_isUnramified
    (D : DegreeData G) (L : FiniteGaloisSubextension K)
    (N : ClosedSubgroup G)
    (hLN : L.field.toSubgroup ≤ N.toSubgroup)
    (hNK : N.toSubgroup ≤ K.toSubgroup)
    (hNunramified : (DegreeData.AbstractExtension.mk N K hNK).IsUnramified D) :
    (L.maximalUnramifiedSubextension D).toSubgroup ≤ N.toSubgroup
theorem

maximalUnramified_normMap_injective

L610 ↗
ClassFormation.FiniteGaloisSubextension.maximalUnramified_normMap_injective
Documentation

In the cyclic case, the lower norm arrow for L / (L ∩ K̃) / K is injective by the order calculation from. This specializes the actual cardinality proof in the reciprocity reduction exact row to the inertia-image intermediate field.

Source context 9 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
Lean source · full declaration
theorem maximalUnramified_normMap_injective
    (A : Rep ℤ G) (hcf : SatisfiesClassFieldAxiom A)
    (D : DegreeData G) (L : FiniteGaloisSubextension K)
    [Finite ((baseField G).toSubgroup ⧸
      extensionSubgroup (baseField G) K (le_baseField K))]
    [IsCyclic L.extensionQuotient] :
    let S := L.inertiaImage D
    let M := L.intermediateField S
    let hLM := L.field_le_intermediateField S
    let hMK := L.intermediateField_le_base S
    letI : Finite
        (M.toSubgroup ⧸ extensionSubgroup M L.field hLM) :=
      L.extension_over_intermediate_finite S
    letI : Finite
        (K.toSubgroup ⧸ extensionSubgroup K M hMK) :=
      L.intermediateField_finite S
    letI : Finite
        (K.toSubgroup ⧸ extensionSubgroup K L.field (hLM.trans hMK)) := by
      simpa only using L.finite
    Function.Injective
      (abstractReciprocityNormMap A K M L.field hLM hMK) := by
  dsimp only
  let S := L.inertiaImage D
  let M := L.intermediateField S
  let hLM := L.field_le_intermediateField S
  let hMK := L.intermediateField_le_base S
  let : (extensionSubgroup K L.field (hLM.trans hMK)).Normal := by
    simpa only using L.normal
  let : (extensionSubgroup K M hMK).Normal :=
    L.intermediateField_normal S inferInstance
  let : Finite
      (K.toSubgroup ⧸ extensionSubgroup K L.field (hLM.trans hMK)) := by
    simpa only using L.finite
  let : Finite
      (M.toSubgroup ⧸ extensionSubgroup M L.field hLM) :=
    L.extension_over_intermediate_finite S
  let : Finite
      (K.toSubgroup ⧸ extensionSubgroup K M hMK) :=
    L.intermediateField_finite S
  let : IsCyclic
      (M.toSubgroup ⧸ extensionSubgroup M L.field hLM) :=
    L.lowerQuotient_isCyclic S
  let : IsCyclic
      (K.toSubgroup ⧸ extensionSubgroup K M hMK) :=
    L.upperQuotient_isCyclic S
  obtain ⟨gKL, hgKL⟩ := IsCyclic.exists_generator
    (α := L.extensionQuotient)
  obtain ⟨gML, hgML⟩ := IsCyclic.exists_generator
    (α := M.toSubgroup ⧸ extensionSubgroup M L.field hLM)
  obtain ⟨gKM, hgKM⟩ := IsCyclic.exists_generator
    (α := K.toSubgroup ⧸ extensionSubgroup K M hMK)
  exact abstractReciprocity_cyclicTower_normMap_injective
    A hcf K M L.field hLM hMK gKL hgKL gML hgML gKM hgKM
theorem

abstractReciprocity_surjective_of_exact_diagram

L670 ↗
ClassFormation.abstractReciprocity_surjective_of_exact_diagram
Documentation

The diagram chase used twice in the first reduction. The middle vertical arrow is surjective when the two outside vertical arrows are surjective, the top-right arrow is surjective, and the bottom row is exact.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
Lean source · statement
theorem abstractReciprocity_surjective_of_exact_diagram
    {Q₀ Q Q₁ B₀ B B₁ : Type*}
    [AddGroup Q₀] [AddGroup Q] [AddGroup Q₁]
    [AddGroup B₀] [AddGroup B] [AddGroup B₁]
    (iQ : Q₀ →+ Q) (pQ : Q →+ Q₁)
    (iB : B₀ →+ B) (pB : B →+ B₁)
    (r₀ : Q₀ →+ B₀) (r : Q →+ B) (r₁ : Q₁ →+ B₁)
    (hexact : Function.Exact iB pB)
    (hpQ : Function.Surjective pQ)
    (hleft : ∀ q, r (iQ q) = iB (r₀ q))
    (hright : ∀ q, pB (r q) = r₁ (pQ q))
    (hr₀ : Function.Surjective r₀)
    (hr₁ : Function.Surjective r₁) :
    Function.Surjective r
theorem

abstractReciprocity_bijective_of_exact_diagram

L707 ↗
ClassFormation.abstractReciprocity_bijective_of_exact_diagram
Documentation

The diagram chase in the third reduction. If both outside reciprocity arrows are bijective and the first lower arrow is injective, then the middle reciprocity arrow is bijective.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
Lean source · statement
theorem abstractReciprocity_bijective_of_exact_diagram
    {Q₀ Q Q₁ B₀ B B₁ : Type*}
    [AddGroup Q₀] [AddGroup Q] [AddGroup Q₁]
    [AddGroup B₀] [AddGroup B] [AddGroup B₁]
    (iQ : Q₀ →+ Q) (pQ : Q →+ Q₁)
    (iB : B₀ →+ B) (pB : B →+ B₁)
    (r₀ : Q₀ →+ B₀) (r : Q →+ B) (r₁ : Q₁ →+ B₁)
    (hexactQ : Function.Exact iQ pQ)
    (hexactB : Function.Exact iB pB)
    (hpQ : Function.Surjective pQ)
    (hiB : Function.Injective iB)
    (hleft : ∀ q, r (iQ q) = iB (r₀ q))
    (hright : ∀ q, pB (r q) = r₁ (pQ q))
    (hr₀ : Function.Bijective r₀)
    (hr₁ : Function.Bijective r₁) :
    Function.Bijective r
theorem

abstractReciprocity_commutator_mem_kernel

L751 ↗
ClassFormation.abstractReciprocity_commutator_mem_kernel
Documentation

Every additive homomorphism from a group into an abelian group kills the commutator subgroup. This is the automatic inclusion in the kernel statement of the first reduction.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
Lean source · statement
theorem abstractReciprocity_commutator_mem_kernel
    {Q : Type*} {B : Type*} [Group Q] [AddCommGroup B]
    (r : Additive Q →+ B) (q : Q)
    (hq : q ∈ commutator Q) :
    r (Additive.ofMul q) = 0
theorem

abstractReciprocity_abelianReduction_kernel

L769 ↗
ClassFormation.abstractReciprocity_abelianReduction_kernel
Documentation

Exact remaining kernel calculation in the first reduction. For the actual maximal abelian intermediate field, commutativity of the right square and injectivity of its reciprocity arrow identify the kernel of the middle arrow with the commutator subgroup.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
Lean source · statement
theorem abstractReciprocity_abelianReduction_kernel
    {K : ClosedSubgroup G} {B : Type*} {C : Type*}
    [AddCommGroup B] [AddCommGroup C]
    (L : FiniteGaloisSubextension K)
    (p : B →+ C)
    (r : Additive L.extensionQuotient →+ B)
    (rAb : Additive
        (K.toSubgroup ⧸ extensionSubgroup K L.abelianIntermediateField
          (L.intermediateField_le_base
            (commutator L.extensionQuotient))) →+ C)
    (hright : ∀ q,
      p (r (Additive.ofMul q)) =
        rAb (Additive.ofMul (L.abelianRestrictionHom q)))
    (hrAb : Function.Injective rAb)
    (q : L.extensionQuotient) :
    r (Additive.ofMul q) = 0 ↔
      q ∈ commutator L.extensionQuotient
theorem

abstractReciprocity_cyclicFactors_injective

L805 ↗
ClassFormation.abstractReciprocity_cyclicFactors_injective
Documentation

The kernel argument in the second reduction. Injectivity of the reciprocity arrows for a jointly faithful family of cyclic quotients forces injectivity of the original arrow. All horizontal maps are the actual restrictions to the intermediate fields cut out by the coordinate kernels.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
universe u
section Representation

-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
  [IsTopologicalGroup G]
Lean source · statement
theorem abstractReciprocity_cyclicFactors_injective
    {K : ClosedSubgroup G} {I : Type*} {C : I → Type*}
    [∀ i, Group (C i)]
    (L : FiniteGaloisSubextension K)
    (f : ∀ i, L.extensionQuotient →* C i)
    (hfaithful : (⨅ i, MonoidHom.ker (f i)) = ⊥)
    {B : Type*} [AddCommGroup B]
    {D : I → Type*} [∀ i, AddCommGroup (D i)]
    (p : ∀ i, B →+ D i)
    (r : Additive L.extensionQuotient →+ B)
    (rFactor : ∀ i,
      Additive
        (K.toSubgroup ⧸ extensionSubgroup K
          (L.intermediateField (MonoidHom.ker (f i)))
          (L.intermediateField_le_base (MonoidHom.ker (f i)))) →+ D i)
    (hright : ∀ i q,
      p i (r (Additive.ofMul q)) =
        rFactor i (Additive.ofMul
          (L.upperRestrictionHom (MonoidHom.ker (f i)) q)))
    (hinjective : ∀ i, Function.Injective (rFactor i)) :
    Function.Injective r

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