Module

Submodule_FiniteAdeleBox.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Submodule_FiniteAdeleBox

9 declarations indexed from sourceView source ↗

Module documentation

Submodule Finite Adele Box

Imports4

Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Mathlib.Algebra.Group.Action.Units
Mathlib.NumberTheory.NumberField.Basic
Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Imported by1

Nyll.AlgebraicCurves.Foundations.Algebra.All

def

finiteAdeleBox

L32 ↗

Submodule.finiteAdeleBox

Documentation

The additive subgroup generated by tensors of lattice elements and integral finite adeles.

Source context 5 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]

Lean source · statement

def finiteAdeleBox (Λ : Submodule ℤ D) : AddSubgroup (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)

def

ofFiniteIdele

L39 ↗

Submodule.ofFiniteIdele

Documentation

The lattice obtained by translating its finite-adele box by the given idele and pulling back diagonally.

Source context 5 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]

Lean source · statement

def ofFiniteIdele (Λ : Submodule ℤ D) (g : (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) : Submodule ℤ D

def

finiteIdeleStabilizer

L47 ↗

Submodule.finiteIdeleStabilizer

Documentation

The subgroup of finite ideles stabilizing the finite-adele box of the lattice.

Source context 5 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]

Lean source · statement

def finiteIdeleStabilizer (Λ : Submodule ℤ D) : Subgroup (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ

def

conjByFiniteIdele

L53 ↗

Submodule.conjByFiniteIdele

Documentation

The lattice obtained by conjugating its finite-adele box and pulling back diagonally.

Source context 5 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]

Lean source · statement

def conjByFiniteIdele (Λ : Submodule ℤ D) (g : (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) :
    Submodule ℤ D

def

finiteIdeleDiagonal

L65 ↗

Submodule.finiteIdeleDiagonal

Documentation

The diagonal homomorphism from algebra units to units after finite-adele extension.

Source context 6 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]
variable (D) in

Lean source · statement

def finiteIdeleDiagonal : Dˣ →* (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ

theorem

val_finiteIdeleDiagonal_apply

L69 ↗

Submodule.val_finiteIdeleDiagonal_apply

Source context 6 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]
variable (D) in

Lean source · statement

theorem val_finiteIdeleDiagonal_apply (d : Dˣ) :
    ((finiteIdeleDiagonal D d : (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) :
      D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ) = (d : D) ⊗ₜ[ℚ] (1 : FiniteAdeleRing (𝓞 ℚ) ℚ)

theorem

mem_ofFiniteIdele_iff

L73 ↗

Submodule.mem_ofFiniteIdele_iff

Source context 6 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]
variable (D) in

Lean source · statement

theorem mem_ofFiniteIdele_iff (Λ : Submodule ℤ D) (g : (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ)
    (z : D) :
    z ∈ ofFiniteIdele Λ g ↔
      z ⊗ₜ[ℚ] (1 : FiniteAdeleRing (𝓞 ℚ) ℚ) ∈
        (finiteAdeleBox Λ).map (AddMonoidHom.mulLeft (g : D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ))

theorem

mem_conjByFiniteIdele_iff

L80 ↗

Submodule.mem_conjByFiniteIdele_iff

Source context 6 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]
variable (D) in

Lean source · statement

theorem mem_conjByFiniteIdele_iff (Λ : Submodule ℤ D) (g : (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ)
    (z : D) :
    z ∈ conjByFiniteIdele Λ g ↔
      z ⊗ₜ[ℚ] (1 : FiniteAdeleRing (𝓞 ℚ) ℚ) ∈
        (finiteAdeleBox Λ).map
          ((AddMonoidHom.mulRight ((g⁻¹ : (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) :
              D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)).comp
            (AddMonoidHom.mulLeft (g : D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)))

theorem

mem_finiteIdeleStabilizer_iff

L90 ↗

Submodule.mem_finiteIdeleStabilizer_iff

Source context 6 commands

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

open scoped TensorProduct Pointwise
open IsDedekindDomain NumberField
noncomputable section
namespace Submodule
variable {D : Type*} [Ring D] [Algebra ℚ D]
variable (D) in

Lean source · statement

theorem mem_finiteIdeleStabilizer_iff (Λ : Submodule ℤ D) (u : (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)ˣ) :
    u ∈ finiteIdeleStabilizer Λ ↔
      u • ((finiteAdeleBox Λ : AddSubgroup (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)) :
          Set (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ))
        = ((finiteAdeleBox Λ : AddSubgroup (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ)) :
          Set (D ⊗[ℚ] FiniteAdeleRing (𝓞 ℚ) ℚ))

Module documentation

Submodule Finite Adele Box

Declarations