Module

NormTowerConductor.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.NormTowerConductor

18 declarations indexed from sourceView source ↗

Module documentation

Norm quotients and narrow finite conductors in a field tower

For a finite tower K ⊂ M ⊂ L, norm transitivity places the actual idele-class norms from L inside those from M. This produces the canonical quotient transition

C_K / N_{L/K} C_L → C_K / N_{M/K} C_M.

The transition is surjective, its kernel is the image of N_{M/K} C_M modulo N_{L/K} C_L, and its orders satisfy the corresponding exact factorization. When both extensions over K are Galois, the narrow finite conductor is contravariant under this inclusion and the conductor support of the intermediate extension is contained in that of the top extension. This is the finite part in the all-real-positive convention, not a claim about the full archimedean conductor.

Imports3

Imported by3

theorem

normTowerIdeleClassIsMulCommutative

L42 ↗

GlobalClassFieldTheory.GlobalClassFields.normTowerIdeleClassIsMulCommutative

Documentation

The canonical commutativity witness used to form ordinary norm quotients.

Source context 5 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField

Lean source · statement

theorem normTowerIdeleClassIsMulCommutative
    {F : Type} [Field F] [NumberField F] :
    IsMulCommutative (IdeleClassGroup F)

theorem

normTowerQuotientIsMulCommutative

L51 ↗

GlobalClassFieldTheory.GlobalClassFields.normTowerQuotientIsMulCommutative

Documentation

Quotient commutativity follows by lifting representatives through the canonical quotient map, without constructing another group dictionary.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative

Lean source · statement

theorem normTowerQuotientIsMulCommutative
    {G : Type*} [Group G] [IsMulCommutative G]
    (N : Subgroup G) : IsMulCommutative (G ⧸ N)

theorem

normTowerIdeleClassQuotientIsMulCommutative

L69 ↗

GlobalClassFieldTheory.GlobalClassFields.normTowerIdeleClassQuotientIsMulCommutative

Documentation

A quotient of the idele class group is commutative, so its norm-image subgroups are normal when forming the second quotient.

Source context 6 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative

Lean source · statement

theorem normTowerIdeleClassQuotientIsMulCommutative
    {F : Type} [Field F] [NumberField F]
    (N : Subgroup (IdeleClassGroup F)) :
    IsMulCommutative (IdeleClassGroup F ⧸ N)

theorem

ideleClassNorm_range_le_of_tower

L93 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_range_le_of_tower

Documentation

Norm transitivity puts every idele-class norm from the top field inside the idele-class norm subgroup of the intermediate field.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]
omit [IsGalois K M] [IsGalois K L] in

Lean source · statement

theorem ideleClassNorm_range_le_of_tower :
    (_root_.ideleClassNorm K L).range ≤
      (_root_.ideleClassNorm K M).range

def

ideleClassNormQuotientTowerMap

L113 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotientTowerMap

Documentation

The quotient transition induced by norm transitivity in a finite field tower.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]

Lean source · statement

def ideleClassNormQuotientTowerMap :
    (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K L).range) →*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K M).range)

theorem

ideleClassNormQuotientTowerMap_mk

L130 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotientTowerMap_mk

Documentation

The tower norm-quotient transition sends an idele class to the same class modulo the intermediate norm subgroup.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]
omit [IsGalois K M] [IsGalois K L] in

Lean source · statement

theorem ideleClassNormQuotientTowerMap_mk
    (x : IdeleClassGroup K) :
    ideleClassNormQuotientTowerMap
        (K := K) (M := M) (L := L)
        (QuotientGroup.mk'
          ((_root_.ideleClassNorm K L).range) x) =
      QuotientGroup.mk'
        ((_root_.ideleClassNorm K M).range) x

theorem

ideleClassNormQuotientTowerMap_surjective

L142 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotientTowerMap_surjective

Documentation

The tower norm-quotient transition is surjective.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]
omit [IsGalois K M] [IsGalois K L] in

Lean source · statement

theorem ideleClassNormQuotientTowerMap_surjective :
    Function.Surjective
      (ideleClassNormQuotientTowerMap
        (K := K) (M := M) (L := L))

def

narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient

L156 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient

Documentation

The narrow-finite-conductor ray class group of the top extension maps canonically onto the norm quotient of the intermediate extension.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]

Lean source · statement

def
    narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient :
    RayClass.RayClassGroup
        (RayClass.Modulus.narrowOfFinite
          (ideleClassNormNarrowFiniteConductor (K := K) (L := L))) →*
      IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K M).range

theorem

narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient_mk

L173 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient_mk

Documentation

The narrow-finite-conductor ray-class map to the intermediate norm quotient sends an idele class to the same class modulo the intermediate norm subgroup.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]
omit [IsGalois K M] in

Lean source · statement

theorem
    narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient_mk
    (x : IdeleClassGroup K) :
    narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient
        (K := K) (M := M) (L := L)
        (QuotientGroup.mk'
          (RayClass.Modulus.congruenceSubgroup
            (RayClass.Modulus.narrowOfFinite
              (ideleClassNormNarrowFiniteConductor
                (K := K) (L := L)))) x) =
      QuotientGroup.mk'
        ((_root_.ideleClassNorm K M).range) x

theorem

narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient_surjective

L203 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient_surjective

Documentation

The narrow-finite-conductor ray-class map to the intermediate norm quotient is surjective.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]
omit [IsGalois K M] in

Lean source · statement

theorem
    narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient_surjective :
    Function.Surjective
      (narrowFiniteConductorRayClassGroupToIntermediateIdeleClassNormQuotient
        (K := K) (M := M) (L := L))

theorem

ideleClassNormQuotientTowerMap_ker

L216 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotientTowerMap_ker

Documentation

The kernel of the tower norm-quotient transition is the image of the intermediate norm subgroup modulo the top norm subgroup.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]
omit [IsGalois K M] [IsGalois K L] in

Lean source · statement

theorem ideleClassNormQuotientTowerMap_ker :
    MonoidHom.ker
        (ideleClassNormQuotientTowerMap
          (K := K) (M := M) (L := L)) =
      Subgroup.map
        (QuotientGroup.mk'
          ((_root_.ideleClassNorm K L).range))
        ((_root_.ideleClassNorm K M).range)

def

ideleClassNormQuotientModuloIntermediateEquiv

L240 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotientModuloIntermediateEquiv

Documentation

Quotienting the top norm quotient by the image of the intermediate norm subgroup gives the intermediate norm quotient.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]

Lean source · statement

def ideleClassNormQuotientModuloIntermediateEquiv :
    ((IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range) ⧸
        Subgroup.map
          (QuotientGroup.mk'
            ((_root_.ideleClassNorm K L).range))
          ((_root_.ideleClassNorm K M).range)) ≃*
      (IdeleClassGroup K ⧸
        (_root_.ideleClassNorm K M).range)

def

narrowFiniteConductorRayClassNormSubgroupQuotientTowerMap

L260 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassNormSubgroupQuotientTowerMap

Documentation

The tower norm-quotient transition transported to the narrow-finite-conductor ray-class norm-subgroup quotient presentations.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]

Lean source · statement

def
    narrowFiniteConductorRayClassNormSubgroupQuotientTowerMap :
    (RayClass.RayClassGroup
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor
              (K := K) (L := L))) ⧸
        Subgroup.map
          (QuotientGroup.mk'
            (RayClass.Modulus.congruenceSubgroup
              (RayClass.Modulus.narrowOfFinite
                (ideleClassNormNarrowFiniteConductor
                  (K := K) (L := L)))))
          ((_root_.ideleClassNorm K L).range)) →*
      (RayClass.RayClassGroup
          (RayClass.Modulus.narrowOfFinite
            (ideleClassNormNarrowFiniteConductor
              (K := K) (L := M))) ⧸
        Subgroup.map
          (QuotientGroup.mk'
            (RayClass.Modulus.congruenceSubgroup
              (RayClass.Modulus.narrowOfFinite
                (ideleClassNormNarrowFiniteConductor
                  (K := K) (L := M)))))
          ((_root_.ideleClassNorm K M).range))

theorem

narrowFiniteConductorRayClassNormSubgroupQuotientTowerMap_commutes

L294 ↗

GlobalClassFieldTheory.GlobalClassFields.narrowFiniteConductorRayClassNormSubgroupQuotientTowerMap_commutes

Documentation

Transporting the tower transition to narrow-finite-conductor ray-class quotient presentations commutes with the canonical identifications with actual norm quotients.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]

Lean source · statement

theorem
    narrowFiniteConductorRayClassNormSubgroupQuotientTowerMap_commutes :
    (narrowFiniteConductorRayClassNormSubgroupQuotientEquivIdeleClassNormQuotient
        (K := K) (L := M)).toMonoidHom.comp
      (narrowFiniteConductorRayClassNormSubgroupQuotientTowerMap
        (K := K) (M := M) (L := L)) =
    (ideleClassNormQuotientTowerMap
        (K := K) (M := M) (L := L)).comp
      (narrowFiniteConductorRayClassNormSubgroupQuotientEquivIdeleClassNormQuotient
        (K := K) (L := L)).toMonoidHom

theorem

ideleClassNormQuotient_card_eq_intermediateNormImage_card_mul_baseNormQuotient_card

L310 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotient_card_eq_intermediateNormImage_card_mul_baseNormQuotient_card

Documentation

The order of the top norm quotient factors into the relative kernel order and the order of the intermediate norm quotient.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]
omit [IsGalois K M] [IsGalois K L] in

Lean source · statement

theorem
    ideleClassNormQuotient_card_eq_intermediateNormImage_card_mul_baseNormQuotient_card :
    Nat.card
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range) =
      Nat.card
          (Subgroup.map
            (QuotientGroup.mk'
              ((_root_.ideleClassNorm K L).range))
            ((_root_.ideleClassNorm K M).range)) *
        Nat.card
          (IdeleClassGroup K ⧸
            (_root_.ideleClassNorm K M).range)

theorem

ideleClassNormQuotient_card_dvd_of_tower

L358 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNormQuotient_card_dvd_of_tower

Documentation

The intermediate norm quotient order divides the top norm quotient order.

Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]
omit [IsGalois K M] [IsGalois K L] in

Lean source · statement

theorem ideleClassNormQuotient_card_dvd_of_tower :
    Nat.card
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K M).range) ∣
      Nat.card
        (IdeleClassGroup K ⧸
          (_root_.ideleClassNorm K L).range)

theorem

ideleClassNorm_narrowFiniteConductor_le_of_tower

L372 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_le_of_tower

Documentation

In a finite Galois tower, the narrow finite conductor of the intermediate norm subgroup is bounded by that of the top norm subgroup.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]

Lean source · statement

theorem ideleClassNorm_narrowFiniteConductor_le_of_tower :
    ideleClassNormNarrowFiniteConductor (K := K) (L := M) ≤
      ideleClassNormNarrowFiniteConductor (K := K) (L := L)

theorem

ideleClassNorm_narrowFiniteConductor_support_subset_of_tower

L385 ↗

GlobalClassFieldTheory.GlobalClassFields.ideleClassNorm_narrowFiniteConductor_support_subset_of_tower

Documentation

In a finite Galois tower, every prime in the narrow finite conductor support of the intermediate norm subgroup also occurs in that of the top norm subgroup.

Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open NumberField
attribute [local instance] normTowerIdeleClassIsMulCommutative
attribute [local instance] normTowerIdeleClassQuotientIsMulCommutative
variable {K : Type} [Field K] [NumberField K]
section Tower
variable
    {M L : Type}
    [Field M] [NumberField M]
    [Field L] [NumberField L]
    [Algebra K M] [Algebra M L] [Algebra K L]
    [IsScalarTower K M L]
    [FiniteDimensional K M] [FiniteDimensional M L]
    [IsGalois K M] [IsGalois K L]

Lean source · statement

theorem ideleClassNorm_narrowFiniteConductor_support_subset_of_tower :
    (ideleClassNormNarrowFiniteConductor (K := K) (L := M)).support ⊆
      (ideleClassNormNarrowFiniteConductor (K := K) (L := L)).support

Module documentation

Norm quotients and narrow finite conductors in a field tower

Declarations