Module

MembershipTypes.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransfer.MembershipTypes

13 declarations indexed from sourceView source ↗

Module documentation

Named membership endpoints for rational finite-norm transport

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

Imports2

Imported by3

instance

membershipTypesIdeleClassGroupIsMulCommutative

L32 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.membershipTypesIdeleClassGroupIsMulCommutative

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

instance

membershipTypesIdeleClassSubgroupNormal

L38 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.membershipTypesIdeleClassSubgroupNormal

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative

Lean source · statement

instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal

def

rationalFiniteNormTransferRelativeNormMembership

L47 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferRelativeNormMembership

Documentation

Membership in the ordinary norm range on the relative K/H/L field spine. The absolute H presentation used by the finite-norm quotient does not occur in this public endpoint.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def rationalFiniteNormTransferRelativeNormMembership
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferExtensionIdeleClass K H hHK) : Prop

def

rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership

L118 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership

Documentation

The named relative norm-membership endpoint for the canonical ordinary extension representative.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
    rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hHKnormal : (extensionSubgroup K H hHK).Normal)
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Prop

def

rationalFiniteNormTransferCanonicalOrdinaryExtensionAbsoluteNormMembership

L146 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalOrdinaryExtensionAbsoluteNormMembership

Documentation

The absolute-H norm-membership endpoint used internally by the finite norm quotient before transport to the relative K/H presentation.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
    rationalFiniteNormTransferCanonicalOrdinaryExtensionAbsoluteNormMembership
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hHKnormal : (extensionSubgroup K H hHK).Normal)
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Prop

def

rationalFiniteNormTransferCanonicalFiniteNormRepresentativeAbsoluteNormMembership

L196 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalFiniteNormRepresentativeAbsoluteNormMembership

Documentation

Absolute norm membership of the canonical representative produced by the finite-norm-class comparison.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
    rationalFiniteNormTransferCanonicalFiniteNormRepresentativeAbsoluteNormMembership
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Prop

structure

RationalFiniteNormTransferCanonicalFiniteNormRepresentativeMembershipData

L248 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferCanonicalFiniteNormRepresentativeMembershipData

Documentation

Packaged absolute membership of the finite-norm representative.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · full declaration

structure RationalFiniteNormTransferCanonicalFiniteNormRepresentativeMembershipData
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Type where
  /-- The packaged finite-norm-representative membership proof. -/
  membership :
    rationalFiniteNormTransferCanonicalFiniteNormRepresentativeAbsoluteNormMembership
      K H L hHK hLH hLHnormal c

def

rationalFiniteNormTransferCanonicalFiniteNormRepresentativeQuotientZero

L274 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalFiniteNormRepresentativeQuotientZero

Documentation

The finite-norm representative and zero have the same named ordinary quotient value.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
    rationalFiniteNormTransferCanonicalFiniteNormRepresentativeQuotientZero
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Prop

structure

RationalFiniteNormTransferCanonicalFiniteNormRepresentativeQuotientZeroData

L313 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferCanonicalFiniteNormRepresentativeQuotientZeroData

Documentation

Packaged quotient-zero comparison for the finite-norm representative.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · full declaration

structure RationalFiniteNormTransferCanonicalFiniteNormRepresentativeQuotientZeroData
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Type where
  /-- The packaged quotient-zero equality. -/
  equality :
    rationalFiniteNormTransferCanonicalFiniteNormRepresentativeQuotientZero
      K H L hHK hLH hLHnormal c

def

rationalFiniteNormTransferCanonicalFiniteNormRepresentativeTargetZero

L339 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.rationalFiniteNormTransferCanonicalFiniteNormRepresentativeTargetZero

Documentation

The named quotient-target zero equality obtained after evaluating the finite-norm quotient equivalence at zero.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · statement

def
    rationalFiniteNormTransferCanonicalFiniteNormRepresentativeTargetZero
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Prop

structure

RationalFiniteNormTransferCanonicalFiniteNormRepresentativeTargetZeroData

L383 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferCanonicalFiniteNormRepresentativeTargetZeroData

Documentation

Packaged quotient-target zero equality for the finite-norm representative.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · full declaration

structure RationalFiniteNormTransferCanonicalFiniteNormRepresentativeTargetZeroData
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Type where
  /-- The packaged target-zero equality. -/
  equality :
    rationalFiniteNormTransferCanonicalFiniteNormRepresentativeTargetZero
      K H L hHK hLH hLHnormal c

structure

RationalFiniteNormTransferCanonicalAbsoluteNormMembershipData

L409 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferCanonicalAbsoluteNormMembershipData

Documentation

Packaged absolute norm membership used to keep the provider proof's dependent field spine out of declaration finalization.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · full declaration

structure RationalFiniteNormTransferCanonicalAbsoluteNormMembershipData
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hHKnormal : (extensionSubgroup K H hHK).Normal)
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Type where
  /-- The packaged absolute norm-membership proof. -/
  membership :
    rationalFiniteNormTransferCanonicalOrdinaryExtensionAbsoluteNormMembership
      K H L hHK hLH hHKnormal hLHnormal c

structure

RationalFiniteNormTransferCanonicalNormMembershipData

L436 ↗

GlobalClassFieldTheory.IdealClassFieldTheory.RationalFiniteNormTransferCanonicalNormMembershipData

Documentation

Packaged relative norm membership used as the final internal provider boundary before exposing the canonical theorem.

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
    membershipTypesIdeleClassGroupIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F) :=
  RationalFiniteNormTransferInternal.ideleClassGroupIsMulCommutative
local instance
    membershipTypesIdeleClassSubgroupNormal
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) : N.Normal :=
  RationalFiniteNormTransferInternal.ideleClassSubgroupNormal N

Lean source · full declaration

structure RationalFiniteNormTransferCanonicalNormMembershipData
    (K H L : ClosedSubgroup
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (hHK : H.toSubgroup ≤ K.toSubgroup)
    (hLH : L.toSubgroup ≤ H.toSubgroup)
    (hHKnormal : (extensionSubgroup K H hHK).Normal)
    (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)]
    [hHLfinite : Finite
      (H.toSubgroup ⧸ extensionSubgroup H L hLH)]
    (c : rationalFiniteNormTransferBaseIdeleClass
      (hKfinite := hKfinite) K) : Type where
  /-- The packaged relative norm-membership proof. -/
  membership :
    rationalFiniteNormTransferCanonicalOrdinaryExtensionNormMembership
      K H L hHK hLH hHKnormal hLHnormal c

Module documentation

Named membership endpoints for rational finite-norm transport

Declarations