NYLL
Module

FiniteNormClass.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransfer.FiniteNormClass
3 declarations indexed from sourceView source ↗

Module documentation

Finite norm-class evaluation after fixed-field inclusion

This compiled leaf preserves the original public declarations while reusing the shared fixed-field instance providers.

Imports2
Imported by2

Declarations

instance

finiteNormClassIdeleClassGroupIsMulCommutative

L32 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.finiteNormClassIdeleClassGroupIsMulCommutative
Source context 8 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory
Lean source · statement
instance
    finiteNormClassIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)
instance

finiteNormClassIdeleClassSubgroupNormal

L38 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.finiteNormClassIdeleClassSubgroupNormal
Source context 9 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory
local instance
    finiteNormClassIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
Lean source · statement
instance
    finiteNormClassIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal
theorem

rationalFiniteNormTransferFiniteNormClass_eq_abstractRepresentative

L48 ↗
GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferFiniteNormClass_eq_abstractRepresentative
Documentation

Transporting a finite norm class after fixed-field inclusion is the canonical norm-quotient class of its named abstract representative. The three fields are supplied directly so clients that already have their finite-extension context do not rebuild an intermediate-subgroup instance tower.

Source context 10 commands

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

noncomputable section
namespace GlobalClassFieldTheory
namespace IdealClassFieldTheory
open ClassFormation
open CyclicCohomology
section RationalIdeleExtension
open Reciprocity
open LocalClassFieldTheory
local instance
    finiteNormClassIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    finiteNormClassIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N
Lean source · statement
theorem rationalFiniteNormTransferFiniteNormClass_eq_abstractRepresentative
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hLHnormal : (extensionSubgroup H L hLH).Normal)
    [hKfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K (le_baseField K))]
    [hKHfinite : Finite
      (K.toSubgroup ⧸ extensionSubgroup K H hHK)]
    [hHfinite : Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          H (le_baseField H))]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (a : KummerTheory.ambientFixedAddSubgroup
      rationalIdeleClassRepresentation K) :
    rationalFiniteNormQuotientEquivIdeleClassNormQuotient
        H L hLH hLHnormal
        (finiteNormClass rationalIdeleClassRepresentation H L hLH
          (fixedFieldInclusion rationalIdeleClassRepresentation
            K H hHK a)) =
      rationalFiniteNormTransferQuotientMap
        H L hLH hLHnormal
        (rationalFiniteNormTransferAbstractRepresentative
          K H hHK a)

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