Module

IntermediateExtension.lean

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.IntermediateExtension

43 declarations indexed from sourceView source ↗

Module documentation

Intermediate extensions from actual quotient subgroups

For the three reductions in the proof of the abstract reciprocity theorem, this file supplies the finite Galois correspondence in the direction used by the construction. If L / K is a packaged finite Galois extension and S ≤ G(L/K), its inverse image in G_K is realized as an actual closed intermediate field M.

Closedness is proved from the explicit decomposition of the inverse image as the finite union of right G_L-cosets. The two Galois-group identifications are then obtained from the actual restriction map and the first and third isomorphism theorems; no correspondence certificate is assumed.

Imports2

Nyll.ClassFieldTheory.AbstractClassFieldTheory.Reciprocity.FiniteGaloisSubextension
Mathlib.Topology.Algebra.Group.Basic

Imported by4

def

intermediateSubgroup

L43 ↗

ClassFormation.FiniteGaloisSubextension.intermediateSubgroup

Documentation

The inverse image in G_K of a subgroup of G(L/K).

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def intermediateSubgroup (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) : Subgroup K.toSubgroup

theorem

mem_intermediateSubgroup_iff

L51 ↗

ClassFormation.FiniteGaloisSubextension.mem_intermediateSubgroup_iff

Documentation

Membership in the intermediate subgroup is characterized by membership of the underlying ambient element.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem mem_intermediateSubgroup_iff
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient)
    (k : K.toSubgroup) :
    k ∈ L.intermediateSubgroup S ↔ L.extensionQuotientMk k ∈ S

theorem

extensionSubgroup_le_intermediateSubgroup

L59 ↗

ClassFormation.FiniteGaloisSubextension.extensionSubgroup_le_intermediateSubgroup

Documentation

The original G_L lies in every inverse-image subgroup.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem extensionSubgroup_le_intermediateSubgroup
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    extensionSubgroup K L.field L.below ≤ L.intermediateSubgroup S

def

intermediateCoset

L72 ↗

ClassFormation.FiniteGaloisSubextension.intermediateCoset

Documentation

The G_L-coset classified by q ∈ G(L/K), defined canonically as a fiber of the quotient map. In particular, its public definition does not choose a representative of q.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def intermediateCoset (L : FiniteGaloisSubextension K)
    (q : L.extensionQuotient) : Set K.toSubgroup

def

representativeIntermediateCoset

L78 ↗

ClassFormation.FiniteGaloisSubextension.representativeIntermediateCoset

Documentation

A representative-based description used only to prove topological facts about the canonical quotient fiber.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def representativeIntermediateCoset (L : FiniteGaloisSubextension K)
    (q : L.extensionQuotient) : Set K.toSubgroup

theorem

mem_intermediateCoset_iff

L86 ↗

ClassFormation.FiniteGaloisSubextension.mem_intermediateCoset_iff

Documentation

Membership in the canonical coset is equality with its quotient class.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem mem_intermediateCoset_iff (L : FiniteGaloisSubextension K)
    (q : L.extensionQuotient) (x : K.toSubgroup) :
    x ∈ L.intermediateCoset q ↔
      L.extensionQuotientMk x = q

theorem

mem_representativeIntermediateCoset_iff

L93 ↗

ClassFormation.FiniteGaloisSubextension.mem_representativeIntermediateCoset_iff

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem mem_representativeIntermediateCoset_iff
    (L : FiniteGaloisSubextension K)
    (q : L.extensionQuotient) (x : K.toSubgroup) :
    x ∈ representativeIntermediateCoset L q ↔
      L.extensionQuotientMk x = q

theorem

intermediateCoset_eq_representativeIntermediateCoset

L130 ↗

ClassFormation.FiniteGaloisSubextension.intermediateCoset_eq_representativeIntermediateCoset

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem intermediateCoset_eq_representativeIntermediateCoset
    (L : FiniteGaloisSubextension K) (q : L.extensionQuotient) :
    L.intermediateCoset q = representativeIntermediateCoset L q

theorem

intermediateSubgroup_eq_iUnion_cosets

L139 ↗

ClassFormation.FiniteGaloisSubextension.intermediateSubgroup_eq_iUnion_cosets

Documentation

The inverse image of S is literally the finite union of the G_L cosets indexed by the elements of S.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem intermediateSubgroup_eq_iUnion_cosets
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    (L.intermediateSubgroup S : Set K.toSubgroup) =
      ⋃ q ∈ (S : Set L.extensionQuotient), L.intermediateCoset q

theorem

representativeIntermediateCoset_isClosed

L156 ↗

ClassFormation.FiniteGaloisSubextension.representativeIntermediateCoset_isClosed

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem representativeIntermediateCoset_isClosed
    (L : FiniteGaloisSubextension K) (q : L.extensionQuotient) :
    IsClosed (representativeIntermediateCoset L q)

theorem

intermediateCoset_isClosed

L165 ↗

ClassFormation.FiniteGaloisSubextension.intermediateCoset_isClosed

Documentation

Every coset in the preceding union is closed: it is the image of the closed subgroup G_L ≤ G_K under right translation.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem intermediateCoset_isClosed (L : FiniteGaloisSubextension K)
    (q : L.extensionQuotient) : IsClosed (L.intermediateCoset q)

theorem

intermediateSubgroup_isClosed

L172 ↗

ClassFormation.FiniteGaloisSubextension.intermediateSubgroup_isClosed

Documentation

Closedness of the inverse image, proved by its finite coset decomposition rather than postulated as a Galois-correspondence property.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem intermediateSubgroup_isClosed (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    IsClosed (L.intermediateSubgroup S : Set K.toSubgroup)

def

intermediateField

L181 ↗

ClassFormation.FiniteGaloisSubextension.intermediateField

Documentation

The closed intermediate field cut out by S ≤ G(L/K).

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · full declaration

def intermediateField (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) : ClosedSubgroup G where
  toSubgroup := (L.intermediateSubgroup S).map K.toSubgroup.subtype
  isClosed' := by
    change IsClosed
      ((fun x : K.toSubgroup => (x : G)) ''
        (L.intermediateSubgroup S : Set K.toSubgroup))
    exact K.isClosed'.isClosedMap_subtype_val _
      (intermediateSubgroup_isClosed L S)

theorem

intermediateField_le_base

L192 ↗

ClassFormation.FiniteGaloisSubextension.intermediateField_le_base

Documentation

The constructed intermediate field lies over K.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem intermediateField_le_base (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    (L.intermediateField S).toSubgroup ≤ K.toSubgroup

theorem

extensionSubgroup_intermediateField_eq

L200 ↗

ClassFormation.FiniteGaloisSubextension.extensionSubgroup_intermediateField_eq

Documentation

Pulling the constructed field back to G_K recovers exactly the inverse-image subgroup.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem extensionSubgroup_intermediateField_eq
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    extensionSubgroup K (L.intermediateField S)
        (L.intermediateField_le_base S) =
      L.intermediateSubgroup S

theorem

field_le_intermediateField

L217 ↗

ClassFormation.FiniteGaloisSubextension.field_le_intermediateField

Documentation

The constructed field is intermediate: L ≤ M.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem field_le_intermediateField (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    L.field.toSubgroup ≤ (L.intermediateField S).toSubgroup

theorem

extensionSubgroup_over_intermediate_eq_comap

L230 ↗

ClassFormation.FiniteGaloisSubextension.extensionSubgroup_over_intermediate_eq_comap

Documentation

The extension subgroup for L/M is the pullback of G_L ◁ G_K along G_M → G_K.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem extensionSubgroup_over_intermediate_eq_comap
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    extensionSubgroup (L.intermediateField S) L.field
        (L.field_le_intermediateField S) =
      (extensionSubgroup K L.field L.below).comap
        (Subgroup.inclusion (L.intermediateField_le_base S))

theorem

extensionSubgroup_over_intermediate_normal

L243 ↗

ClassFormation.FiniteGaloisSubextension.extensionSubgroup_over_intermediate_normal

Documentation

L/M is normal because it is obtained by restricting the normal subgroup G_L ◁ G_K to G_M.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem extensionSubgroup_over_intermediate_normal
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    (extensionSubgroup (L.intermediateField S) L.field
      (L.field_le_intermediateField S)).Normal

instance

extensionSubgroup_over_intermediate_normalInstance

L251 ↗

ClassFormation.FiniteGaloisSubextension.extensionSubgroup_over_intermediate_normalInstance

Documentation

The extension subgroup over an intermediate field is normal in the intermediate subgroup.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

instance extensionSubgroup_over_intermediate_normalInstance
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    (extensionSubgroup (L.intermediateField S) L.field
      (L.field_le_intermediateField S)).Normal

theorem

extension_over_intermediate_finite

L258 ↗

ClassFormation.FiniteGaloisSubextension.extension_over_intermediate_finite

Documentation

The lower extension L/M is finite.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem extension_over_intermediate_finite
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    Finite ((L.intermediateField S).toSubgroup ⧸
      extensionSubgroup (L.intermediateField S) L.field
        (L.field_le_intermediateField S))

theorem

intermediateField_finite

L271 ↗

ClassFormation.FiniteGaloisSubextension.intermediateField_finite

Documentation

The intermediate extension M/K is finite, since its subgroup contains the finite-index subgroup G_L.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem intermediateField_finite
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    Finite (K.toSubgroup ⧸ extensionSubgroup K (L.intermediateField S)
      (L.intermediateField_le_base S))

def

intermediateFiniteAbstractExtension

L287 ↗

ClassFormation.FiniteGaloisSubextension.intermediateFiniteAbstractExtension

Documentation

The generally non-Galois finite extension L^S/K attached to an arbitrary subgroup S ≤ G(L/K). Normality is deliberately absent from this bundle; clients that only need finite-extension invariants should use this rather than forcing S through intermediateFiniteGalois.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · full declaration

def intermediateFiniteAbstractExtension
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    DegreeData.FiniteAbstractExtension G where
  field := L.intermediateField S
  base := K
  below := L.intermediateField_le_base S
  finiteQuotient := L.intermediateField_finite S

theorem

intermediateSubgroup_normal

L297 ↗

ClassFormation.FiniteGaloisSubextension.intermediateSubgroup_normal

Documentation

A normal subgroup S ◁ G(L/K) has normal inverse image in G_K.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem intermediateSubgroup_normal
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient)
    (hS : S.Normal) : (L.intermediateSubgroup S).Normal

theorem

intermediateField_normal

L304 ↗

ClassFormation.FiniteGaloisSubextension.intermediateField_normal

Documentation

Hence M/K is normal whenever S is normal.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem intermediateField_normal
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient)
    (hS : S.Normal) :
    (extensionSubgroup K (L.intermediateField S)
      (L.intermediateField_le_base S)).Normal

def

lowerFiniteGalois

L313 ↗

ClassFormation.FiniteGaloisSubextension.lowerFiniteGalois

Documentation

The actual finite Galois extension L/M.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · full declaration

def lowerFiniteGalois (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    FiniteGaloisSubextension (L.intermediateField S) where
  field := L.field
  below := L.field_le_intermediateField S
  normal := L.extensionSubgroup_over_intermediate_normal S
  finite := L.extension_over_intermediate_finite S

def

intermediateFiniteGalois

L322 ↗

ClassFormation.FiniteGaloisSubextension.intermediateFiniteGalois

Documentation

If S is normal, the actual finite Galois extension M/K.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · full declaration

def intermediateFiniteGalois (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) (hS : S.Normal) :
    FiniteGaloisSubextension K where
  field := L.intermediateField S
  below := L.intermediateField_le_base S
  normal := L.intermediateField_normal S hS
  finite := L.intermediateField_finite S

def

lowerRestrictionHom

L333 ↗

ClassFormation.FiniteGaloisSubextension.lowerRestrictionHom

Documentation

Restriction from G_M to the subgroup S ≤ G(L/K). The codomain membership proof is supplied by the defining inverse-image equation for M.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def lowerRestrictionHom (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    (L.intermediateField S).toSubgroup →* S

theorem

lowerRestrictionHom_apply_coe

L351 ↗

ClassFormation.FiniteGaloisSubextension.lowerRestrictionHom_apply_coe

Documentation

The lower restriction homomorphism evaluates by restricting the underlying ambient automorphism.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem lowerRestrictionHom_apply_coe (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient)
    (m : (L.intermediateField S).toSubgroup) :
    ((L.lowerRestrictionHom S m : S) : L.extensionQuotient) =
      L.extensionQuotientMk
        (Subgroup.inclusion (L.intermediateField_le_base S) m)

theorem

lowerRestrictionHom_surjective

L361 ↗

ClassFormation.FiniteGaloisSubextension.lowerRestrictionHom_surjective

Documentation

Every element of S is represented by an element of G_M; hence the restriction map is onto.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem lowerRestrictionHom_surjective (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    Function.Surjective (L.lowerRestrictionHom S)

theorem

lowerRestrictionHom_ker

L379 ↗

ClassFormation.FiniteGaloisSubextension.lowerRestrictionHom_ker

Documentation

The kernel of restriction is exactly G_L viewed inside G_M.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem lowerRestrictionHom_ker (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    MonoidHom.ker (L.lowerRestrictionHom S) =
      extensionSubgroup (L.intermediateField S) L.field
        (L.field_le_intermediateField S)

def

lowerQuotientEquiv

L411 ↗

ClassFormation.FiniteGaloisSubextension.lowerQuotientEquiv

Documentation

The first actual Galois-group identification used: G(L/M) ≃ S.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def lowerQuotientEquiv (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) :
    (L.lowerFiniteGalois S).extensionQuotient ≃* S

theorem

lowerQuotientEquiv_mk

L425 ↗

ClassFormation.FiniteGaloisSubextension.lowerQuotientEquiv_mk

Documentation

Representative formula for G(L/M) ≃ S.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem lowerQuotientEquiv_mk (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient)
    (m : (L.intermediateField S).toSubgroup) :
    L.lowerQuotientEquiv S
        ((L.lowerFiniteGalois S).extensionQuotientMk m) =
      L.lowerRestrictionHom S m

theorem

lowerQuotientEquiv_mk_coe

L445 ↗

ClassFormation.FiniteGaloisSubextension.lowerQuotientEquiv_mk_coe

Documentation

The same representative formula after forgetting the subtype S; this is the form used when composing restriction maps in the reduction diagram.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem lowerQuotientEquiv_mk_coe (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient)
    (m : (L.intermediateField S).toSubgroup) :
    ((L.lowerQuotientEquiv S
        ((L.lowerFiniteGalois S).extensionQuotientMk m) : S) :
          L.extensionQuotient) =
      L.extensionQuotientMk
        ⟨m.1, L.intermediateField_le_base S m.property⟩

theorem

intermediateSubgroup_map_quotient_eq

L460 ↗

ClassFormation.FiniteGaloisSubextension.intermediateSubgroup_map_quotient_eq

Documentation

Mapping the inverse image of S back to G(L/K) recovers S itself.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem intermediateSubgroup_map_quotient_eq
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient) :
    (L.intermediateSubgroup S).map L.extensionQuotientMk = S

instance

intermediateSubgroup_normalInstance

L467 ↗

ClassFormation.FiniteGaloisSubextension.intermediateSubgroup_normalInstance

Documentation

The subgroup attached to the intermediate extension is normal.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

instance intermediateSubgroup_normalInstance
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient)
    [hS : S.Normal] : (L.intermediateSubgroup S).Normal

instance

intermediateField_normalInstance

L473 ↗

ClassFormation.FiniteGaloisSubextension.intermediateField_normalInstance

Documentation

The field represented by a normal intermediate subgroup is a normal subextension.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

instance intermediateField_normalInstance
    (L : FiniteGaloisSubextension K) (S : Subgroup L.extensionQuotient)
    [hS : S.Normal] :
    (extensionSubgroup K (L.intermediateField S)
      (L.intermediateField_le_base S)).Normal

def

upperQuotient

L482 ↗

ClassFormation.FiniteGaloisSubextension.upperQuotient

Documentation

The third-isomorphism identification used in the normal-subextension diagram: G(L/K)/S ≃ G(M/K).

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def upperQuotient (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) : Type _

instance

upperQuotient_groupInstance

L487 ↗

ClassFormation.FiniteGaloisSubextension.upperQuotient_groupInstance

Documentation

The upper quotient over an intermediate field carries its canonical group structure.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

instance upperQuotient_groupInstance (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] :
    Group (L.upperQuotient S)

def

upperQuotientMulEquiv

L494 ↗

ClassFormation.FiniteGaloisSubextension.upperQuotientMulEquiv

Documentation

Comparison with the group-library presentation of the upper quotient.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def upperQuotientMulEquiv (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] :
    L.upperQuotient S ≃* (L.extensionQuotient ⧸ S)

def

upperQuotientMk

L500 ↗

ClassFormation.FiniteGaloisSubextension.upperQuotientMk

Documentation

The canonical projection to the named upper quotient.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def upperQuotientMk (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] :
    L.extensionQuotient →* L.upperQuotient S

theorem

upperQuotientMk_apply

L508 ↗

ClassFormation.FiniteGaloisSubextension.upperQuotientMk_apply

Documentation

The named upper quotient projection agrees with the underlying quotient-group projection.

Source context 8 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}
omit [IsTopologicalGroup G] in

Lean source · statement

theorem upperQuotientMk_apply (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal]
    (q : L.extensionQuotient) :
    L.upperQuotientMulEquiv S (L.upperQuotientMk S q) =
      (QuotientGroup.mk q : L.extensionQuotient ⧸ S)

def

upperQuotientEquiv

L517 ↗

ClassFormation.FiniteGaloisSubextension.upperQuotientEquiv

Documentation

The third-isomorphism identification, with both source and target kept behind their named finite-Galois quotient boundaries.

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

def upperQuotientEquiv (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] :
    L.upperQuotient S ≃*
      (L.intermediateFiniteGalois S inferInstance).extensionQuotient

theorem

upperQuotientEquiv_mk_mk

L540 ↗

ClassFormation.FiniteGaloisSubextension.upperQuotientEquiv_mk_mk

Documentation

Representative formula for G(L/K)/S ≃ G(M/K).

Source context 7 commands

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

namespace ClassFormation
open KummerTheory
open CyclicCohomology
noncomputable section
variable {G : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
namespace FiniteGaloisSubextension
variable {K : ClosedSubgroup G}

Lean source · statement

theorem upperQuotientEquiv_mk_mk (L : FiniteGaloisSubextension K)
    (S : Subgroup L.extensionQuotient) [S.Normal] (k : K.toSubgroup) :
    L.upperQuotientEquiv S
        (L.upperQuotientMk S (L.extensionQuotientMk k)) =
      (L.intermediateFiniteGalois S inferInstance).extensionQuotientMk k

Module documentation

Intermediate extensions from actual quotient subgroups

Declarations