NYLL
Module

FiniteAbelianClassFieldCorrespondence.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.GlobalClassFields.FiniteAbelianClassFieldCorrespondence
11 declarations indexed from sourceView source ↗

Module documentation

The ordinary finite abelian class-field correspondence

The abstract finite abelian classification is formulated on the fixed parts of the rational absolute idele-class representation. For a finite abstract base field, the canonical fixed-field comparison transports its norm subgroups to the ordinary idele class group of the actual fixed number field.

This file records that transported correspondence. In particular, the two lattice formulas are now equalities of ordinary determinant-norm subgroups: composita correspond to intersections and intersection fields correspond to products.

Imports4
Imported by3

Declarations

instance

finiteAbelianClassFieldCorrespondence_separableClosureAlgebra

L43 ↗
GlobalClassFieldTheory.GlobalClassFields.finiteAbelianClassFieldCorrespondence_separableClosureAlgebra
Documentation

Fix the rational algebra structure used by every occurrence of the absolute Galois group in this module.

Source context 8 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
Lean source · statement
instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ)
instance

ordinaryFixedFieldBaseQuotientFinite

L52 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryFixedFieldBaseQuotientFinite
Source context 10 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
Lean source · statement
instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field))
instance

ordinaryFixedFieldFiniteDimensional

L62 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryFixedFieldFiniteDimensional
Source context 11 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
Lean source · statement
instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
instance

ordinaryFixedFieldNumberField

L68 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryFixedFieldNumberField
Source context 12 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
noncomputable local instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
Lean source · statement
instance ordinaryFixedFieldNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
def

ordinaryIdeleClassNormSubgroup

L82 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup
Documentation

The ordinary idele-class norm subgroup represented by a finite abelian subextension of a rational absolute fixed field.

The definition transports the abstract norm subgroup through the canonical equivalence from the ordinary idele class group of the actual fixed field. The theorem ordinaryIdeleClassNormSubgroup_eq_actualNormRange below identifies it with the genuine determinant-norm range of the represented extension.

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
noncomputable local instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance ordinaryFixedFieldNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
Lean source · statement
def ordinaryIdeleClassNormSubgroup
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    AddSubgroup
      (Additive
        (IdeleClassGroup
          (abstractFixedField
            ℚ (SeparableClosure ℚ) K.field)))
theorem

ordinaryIdeleClassNormSubgroup_eq_map

L96 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_eq_map
Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
noncomputable local instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance ordinaryFixedFieldNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
Lean source · statement
theorem ordinaryIdeleClassNormSubgroup_eq_map
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    ordinaryIdeleClassNormSubgroup K L =
      (L.normSubgroup rationalIdeleClassRepresentation).map
        (rationalAbstractFixedFieldIdeleClassEquivFixed
          K.field).symm.toAddMonoidHom
theorem

ordinaryIdeleClassNormSubgroup_eq_actualNormRange

L108 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_eq_actualNormRange
Documentation

The transported subgroup is the genuine ordinary determinant-norm range of the actual relative fixed-field extension.

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
noncomputable local instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance ordinaryFixedFieldNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
Lean source · full declaration
theorem ordinaryIdeleClassNormSubgroup_eq_actualNormRange
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L : FiniteAbelianSubextension K.field) :
    let F :=
      abstractFixedField ℚ (SeparableClosure ℚ) K.field
    let E :=
      abstractRelativeFixedField
        ℚ (SeparableClosure ℚ) L.below
    letI hKfinite : Finite
        ((baseField
          (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
          CyclicCohomology.extensionSubgroup
            (baseField
              (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
            K.field (le_baseField K.field)) :=
      K.finite
    letI hLfinite : Finite
        (K.field.toSubgroup ⧸
          CyclicCohomology.extensionSubgroup K.field L.field L.below) :=
      L.finite
    letI : FiniteDimensional ℚ F :=
      abstractFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ) K.field hKfinite
    letI : FiniteDimensional F E :=
      abstractRelativeFixedField_finiteDimensional
        ℚ (SeparableClosure ℚ)
        K.field L.field L.below hKfinite hLfinite
    letI : IsScalarTower ℚ F E :=
      IsScalarTower.of_algebraMap_eq' rfl
    letI : FiniteDimensional ℚ E :=
      FiniteDimensional.trans ℚ F E
    letI : NumberField F :=
      NumberField.of_module_finite ℚ F
    letI : NumberField E :=
      NumberField.of_module_finite ℚ E
    letI : IsAbelianGalois F E :=
      finiteAbelianSubextensionAbstractRelativeFixedFieldIsAbelianGalois L
    ordinaryIdeleClassNormSubgroup K L =
      (_root_.ideleClassNorm F E).range.toAddSubgroup := by
  exact
    (ordinaryIdeleClassNormSubgroup_eq_map K L).trans
      (map_rationalFiniteNormSubgroup_eq_ordinaryIdeleClassNormRange_concrete
        (hKfinite := K.finite) (hfinite := L.finite)
        K.field L.field L.below L.normal)
theorem

le_iff_ordinaryIdeleClassNormSubgroup_le

L156 ↗
GlobalClassFieldTheory.GlobalClassFields.le_iff_ordinaryIdeleClassNormSubgroup_le
Documentation

Field inclusion is exactly reverse inclusion of the represented ordinary determinant-norm subgroups.

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
noncomputable local instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance ordinaryFixedFieldNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
Lean source · statement
theorem le_iff_ordinaryIdeleClassNormSubgroup_le
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L₁ L₂ : FiniteAbelianSubextension K.field) :
    L₁ ≤ L₂ ↔
      ordinaryIdeleClassNormSubgroup K L₂ ≤
        ordinaryIdeleClassNormSubgroup K L₁
theorem

ordinaryIdeleClassNormSubgroup_injective

L200 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_injective
Documentation

A finite abelian subextension is uniquely determined by its ordinary idele-class norm subgroup.

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
noncomputable local instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance ordinaryFixedFieldNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
Lean source · statement
theorem ordinaryIdeleClassNormSubgroup_injective
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)) :
    Function.Injective
      (ordinaryIdeleClassNormSubgroup K)
theorem

ordinaryIdeleClassNormSubgroup_compositum

L216 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_compositum
Documentation

The ordinary norm subgroup of a compositum is the intersection of the two ordinary norm subgroups.

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
noncomputable local instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance ordinaryFixedFieldNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
Lean source · statement
theorem ordinaryIdeleClassNormSubgroup_compositum
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L₁ L₂ : FiniteAbelianSubextension K.field) :
    ordinaryIdeleClassNormSubgroup K (L₁.compositum L₂) =
      ordinaryIdeleClassNormSubgroup K L₁ ⊓
        ordinaryIdeleClassNormSubgroup K L₂
theorem

ordinaryIdeleClassNormSubgroup_intersection

L276 ↗
GlobalClassFieldTheory.GlobalClassFields.ordinaryIdeleClassNormSubgroup_intersection
Documentation

The ordinary norm subgroup of an intersection field is the product of the two ordinary norm subgroups.

Source context 13 commands

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

open scoped NumberField
noncomputable section
namespace GlobalClassFieldTheory
namespace GlobalClassFields
open ClassFormation
open KummerTheory
open LocalClassFieldTheory
open Reciprocity
/-- Fix the rational algebra structure used by every occurrence of the
absolute Galois group in this module. -/
noncomputable local instance
    finiteAbelianClassFieldCorrespondence_separableClosureAlgebra :
    Algebra ℚ (SeparableClosure ℚ) :=
  rationalSeparableClosureAlgebra
variable
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
local instance ordinaryFixedFieldBaseQuotientFinite :
    Finite
      ((baseField
        (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ)).toSubgroup ⧸
        CyclicCohomology.extensionSubgroup
          (baseField
            (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
          K.field (le_baseField K.field)) :=
  K.finite
noncomputable local instance ordinaryFixedFieldFiniteDimensional :
    FiniteDimensional ℚ
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  abstractFixedField_finiteDimensional
    ℚ (SeparableClosure ℚ) K.field K.finite
noncomputable local instance ordinaryFixedFieldNumberField :
    NumberField
      (abstractFixedField ℚ (SeparableClosure ℚ) K.field) :=
  NumberField.of_module_finite ℚ
    (abstractFixedField ℚ (SeparableClosure ℚ) K.field)
Lean source · statement
theorem ordinaryIdeleClassNormSubgroup_intersection
    (K : FiniteAbstractField
      (SeparableClosure ℚ ≃ₐ[ℚ] SeparableClosure ℚ))
    (L₁ L₂ : FiniteAbelianSubextension K.field) :
    ordinaryIdeleClassNormSubgroup K (L₁.intersection L₂) =
      ordinaryIdeleClassNormSubgroup K L₁ ⊔
        ordinaryIdeleClassNormSubgroup K L₂

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