NYLL
Module

ClosedFiniteIndexClassFieldNormRange.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.ClosedFiniteIndexClassFieldNormRange
6 declarations indexed from sourceView source ↗

Module documentation

Norm range over the canonical fixed-field base

This leaf compares the selected abstract norm subgroup with the actual idèle-class norm range over the canonical fixed-field base.

Imports1
Imported by2

Declarations

theorem

subgroup_map_toAddSubgroup_mulEquiv

L32 ↗
GlobalClassFieldTheory.GlobalClassFields.subgroup_map_toAddSubgroup_mulEquiv
Documentation

Opaque bridge from multiplicative subgroup transport to its additive presentation. Keeping this generic prevents concrete fixed-field endpoints from being unfolded by rw while comparing the two presentations.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem subgroup_map_toAddSubgroup_mulEquiv
    {G G₂ : Type*} [Group G] [Group G₂]
    (S : Subgroup G) (e : G ≃* G₂) :
    (S.map e.toMonoidHom).toAddSubgroup =
      S.toAddSubgroup.map
        (MulEquiv.toAdditive e).toAddMonoidHom
def

closedFiniteIndexClassFieldIdeleClassEquiv

L43 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassFieldIdeleClassEquiv
Documentation

The idèle-class transport attached to the selected base equivalence. Naming this endpoint once keeps the fixed-field instance tower out of downstream definitional-equality checks.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
def closedFiniteIndexClassFieldIdeleClassEquiv
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    IdeleClassGroup K ≃*
      IdeleClassGroup
        (closedFiniteIndexClassFieldBase
          (K := K) H hclosed)
theorem

closedFiniteIndexClassField_ideleClassNorm_range_toAddSubgroup

L57 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField_ideleClassNorm_range_toAddSubgroup
Documentation

Additive form of the selected class-field norm-range computation, with the concrete idèle-class endpoint hidden behind one typed definition.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem closedFiniteIndexClassField_ideleClassNorm_range_toAddSubgroup
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    (_root_.ideleClassNorm
      (closedFiniteIndexClassFieldBase
        (K := K) H hclosed)
      (closedFiniteIndexClassField
        (K := K) H hclosed)).range.toAddSubgroup =
      H.toAddSubgroup.map
        (MulEquiv.toAdditive
          (closedFiniteIndexClassFieldIdeleClassEquiv
            (K := K) H hclosed)).toAddMonoidHom
theorem

ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassField_eq_range

L83 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassField_eq_range
Documentation

The represented abstract norm subgroup as the same named actual norm range. This wrapper uses the lightweight named-field API, avoiding the dependent letI tower in the raw fixed-field comparison theorem.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem
    ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassField_eq_range
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    ordinaryIdeleClassNormSubgroup
        (closedFiniteIndexClassFieldReciprocityFiniteAbstractField
          (K := K) H hclosed)
        (closedFiniteIndexClassFieldSubextension
          (K := K) H hclosed) =
      (_root_.ideleClassNorm
        (closedFiniteIndexClassFieldBase
          (K := K) H hclosed)
        (closedFiniteIndexClassField
          (K := K) H hclosed)).range.toAddSubgroup
theorem

closedFiniteIndexClassField_ideleClassNorm_range_over_base

L109 ↗
GlobalClassFieldTheory.GlobalClassFields.closedFiniteIndexClassField_ideleClassNorm_range_over_base
Documentation

Over the canonical fixed-field base, the determinant-norm range of the selected class field is the transport of H.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem closedFiniteIndexClassField_ideleClassNorm_range_over_base
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    (_root_.ideleClassNorm
      (closedFiniteIndexClassFieldBase
        (K := K) H hclosed)
      (closedFiniteIndexClassField
        (K := K) H hclosed)).range =
      H.map
        (ideleClassCongr
          (closedFiniteIndexClassFieldBaseEquiv
            (K := K) H hclosed)).toMonoidHom
theorem

ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassFieldSubextension

L165 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassFieldSubextension
Documentation

The selected subextension is a literal preimage of the transported closed finite-index subgroup under the ordinary norm-subgroup correspondence.

Source context 6 commands

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

open scoped IsMulCommutative NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open Reciprocity
variable {K : Type} [Field K] [NumberField K]
Lean source · statement
theorem
    ordinaryIdeleClassNormSubgroup_closedFiniteIndexClassFieldSubextension
    (H : Subgroup (IdeleClassGroup K))
    (hclosed : IsClosed (H : Set (IdeleClassGroup K)))
    [H.FiniteIndex] :
    ordinaryIdeleClassNormSubgroup
        (closedFiniteIndexClassFieldReciprocityFiniteAbstractField
          (K := K) H hclosed)
        (closedFiniteIndexClassFieldSubextension
          (K := K) H hclosed) =
      H.toAddSubgroup.map
        (MulEquiv.toAdditive
          (ideleClassCongr
            (closedFiniteIndexClassFieldBaseEquiv
              (K := K) H hclosed))).toAddMonoidHom

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