Module

RestrictedProductUnitsTopology.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Idele.RestrictedProductUnitsTopology

4 declarations indexed from sourceView source ↗

Module documentation

Topology on units of a restricted product

For the cofinite restricted product, Mathlib's algebraic unitsEquiv is a topological group equivalence when each distinguished local submonoid is open. The units on the left carry their graph topology; the right side has the restricted-product topology of the local unit groups.

Imports3

Mathlib.Topology.Algebra.Group.Units
Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Mathlib.Topology.Algebra.RestrictedProduct.Units

Imported by2

def

inclusionMonoidHom

L35 ↗

RestrictedProduct.inclusionMonoidHom

Source context 8 commands

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

open Filter
open scoped RestrictedProduct
noncomputable section
namespace RestrictedProduct
universe u v w
variable {ι : Type u} {R : ι → Type v}
  [∀ i, Monoid (R i)] [∀ i, TopologicalSpace (R i)]
variable {S : ι → Type w}
  [∀ i, SetLike (S i) (R i)] [∀ i, SubmonoidClass (S i) (R i)]
variable {B : ∀ i, S i}

Lean source · full declaration

def inclusionMonoidHom {𝓕 𝓖 : Filter ι} (h : 𝓕 ≤ 𝓖) :
    (Πʳ i, [R i, B i]_[𝓖]) →* (Πʳ i, [R i, B i]_[𝓕]) where
  toFun := inclusion R (fun i => (B i : Set (R i))) h
  map_one' := rfl
  map_mul' _ _ := rfl

def

unitsEquivPrincipal

L43 ↗

RestrictedProduct.unitsEquivPrincipal

Documentation

At a principal filter, the algebraic equivalence of units is already a topological group equivalence; no openness assumption is needed.

Source context 8 commands

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

open Filter
open scoped RestrictedProduct
noncomputable section
namespace RestrictedProduct
universe u v w
variable {ι : Type u} {R : ι → Type v}
  [∀ i, Monoid (R i)] [∀ i, TopologicalSpace (R i)]
variable {S : ι → Type w}
  [∀ i, SetLike (S i) (R i)] [∀ i, SubmonoidClass (S i) (R i)]
variable {B : ∀ i, S i}

Lean source · statement

def unitsEquivPrincipal (T : Set ι) :
    (Πʳ i, [R i, B i]_[𝓟 T])ˣ ≃ₜ*
      (Πʳ i, [(R i)ˣ, (Submonoid.ofClass (B i)).units]_[𝓟 T])

theorem

isOpenEmbedding_units_inclusion

L82 ↗

RestrictedProduct.isOpenEmbedding_units_inclusion

Documentation

The principal-stage inclusion of ring restricted products induces an open embedding of their unit groups when the distinguished submonoids are open.

Source context 8 commands

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

open Filter
open scoped RestrictedProduct
noncomputable section
namespace RestrictedProduct
universe u v w
variable {ι : Type u} {R : ι → Type v}
  [∀ i, Monoid (R i)] [∀ i, TopologicalSpace (R i)]
variable {S : ι → Type w}
  [∀ i, SetLike (S i) (R i)] [∀ i, SubmonoidClass (S i) (R i)]
variable {B : ∀ i, S i}

Lean source · statement

theorem isOpenEmbedding_units_inclusion
    (hBopen : ∀ i, IsOpen (B i : Set (R i)))
    {T : Set ι} (hT : cofinite ≤ 𝓟 T) :
    Topology.IsOpenEmbedding (Units.map (inclusionMonoidHom (B := B) hT))

def

unitsContinuousMulEquiv

L96 ↗

RestrictedProduct.unitsContinuousMulEquiv

Documentation

For open distinguished local submonoids, Mathlib's restricted-product unit equivalence is an equivalence of topological groups.

Source context 8 commands

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

open Filter
open scoped RestrictedProduct
noncomputable section
namespace RestrictedProduct
universe u v w
variable {ι : Type u} {R : ι → Type v}
  [∀ i, Monoid (R i)] [∀ i, TopologicalSpace (R i)]
variable {S : ι → Type w}
  [∀ i, SetLike (S i) (R i)] [∀ i, SubmonoidClass (S i) (R i)]
variable {B : ∀ i, S i}

Lean source · statement

def unitsContinuousMulEquiv
    (hBopen : ∀ i, IsOpen (B i : Set (R i))) :
    (Πʳ i, [R i, B i])ˣ ≃ₜ*
      (Πʳ i, [(R i)ˣ, (Submonoid.ofClass (B i)).units])

Module documentation

Topology on units of a restricted product

Declarations

inclusionMonoidHom

unitsEquivPrincipal

isOpenEmbedding_units_inclusion

unitsContinuousMulEquiv