NYLL
Module

AlgebraicLocalizationTopology.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.AlgebraicLocalizationTopology
14 declarations indexed from sourceView source ↗

Module documentation

Topological decomposition--localization comparison

The algebraic localization comparison is algebraically a MulEquiv. This file establishes its finite-support continuity input: fixing one element of the algebraic localization only requires fixing finitely many elements of the original algebraic extension.

Imports3
Imported by2

Declarations

instance

generalLocalizationBaseAlgebra

L36 ↗
ClassFieldTower.Martinet.Shafarevich.generalLocalizationBaseAlgebra
Source context 11 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
Lean source · statement
instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion
instance

generalLocalizationBaseSMul

L39 ↗
ClassFieldTower.Martinet.Shafarevich.generalLocalizationBaseSMul
Source context 12 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
Lean source · statement
instance generalLocalizationBaseSMul : SMul K w.1.Completion
instance

generalLocalizationCompletionAlgebra

L42 ↗
ClassFieldTower.Martinet.Shafarevich.generalLocalizationCompletionAlgebra
Source context 13 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
Lean source · statement
instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion
abbrev

localization

L46 ↗
ClassFieldTower.Martinet.Shafarevich.localization
Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
abbrev localization
theorem

algebraicLocalization_fixing_finite_support

L53 ↗
ClassFieldTower.Martinet.Shafarevich.algebraicLocalization_fixing_finite_support
Documentation

The action on any one algebraic-localization element is controlled by finitely many elements of the original algebraic extension. This is the pointwise source for continuity of the decomposition--localization comparison in the Krull topologies.

Source context 15 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
omit [IsGalois K L] in
Lean source · statement
theorem algebraicLocalization_fixing_finite_support
    (z : localization vK w) :
    ∃ S : Finset L, ∀ σ : absoluteValueDecompositionGroup K w.1,
      (∀ x ∈ S, (σ.1 : L ≃ₐ[K] L) x = x) →
        decompositionGroupToLocalization vK hvK w σ z = z
def

decompositionGroupToAlgebraicLocalizationMonoidHom

L102 ↗
ClassFieldTower.Martinet.Shafarevich.decompositionGroupToAlgebraicLocalizationMonoidHom
Documentation

The algebraic decomposition--localization comparison as a monoid homomorphism.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
def decompositionGroupToAlgebraicLocalizationMonoidHom :
    absoluteValueDecompositionGroup K w.1 →*
      (localization vK w ≃ₐ[vK.Completion] localization vK w)
theorem

algEquiv_fix_of_fin_generates

L107 ↗
ClassFieldTower.Martinet.Shafarevich.algEquiv_fix_of_fin_generates
Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
theorem algEquiv_fix_of_fin_generates
    {F A : Type*} [Field F] [Field A] [Algebra F A]
    (E : IntermediateField F A) {n : ℕ} (b : Fin n → E)
    (hb : Submodule.span F (Set.range b) = ⊤)
    (sigma : A ≃ₐ[F] A)
    (hsigma : ∀ i, sigma (b i : A) = b i) (z : E) :
    sigma (z : A) = z
theorem

absoluteValueDecompositionGroup_fixing_finset_mem_nhds

L120 ↗
ClassFieldTower.Martinet.Shafarevich.absoluteValueDecompositionGroup_fixing_finset_mem_nhds
Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
theorem absoluteValueDecompositionGroup_fixing_finset_mem_nhds
    (S : Finset L) :
    {sigma : absoluteValueDecompositionGroup K w.1 |
      ∀ x ∈ S, (sigma.1 : L ≃ₐ[K] L) x = x} ∈ 𝓝 1
def

algebraicLocalizationStabilizerSubgroup

L137 ↗
ClassFieldTower.Martinet.Shafarevich.algebraicLocalizationStabilizerSubgroup
Documentation

The subgroup of the decomposition group fixing one algebraic-localization element.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
def algebraicLocalizationStabilizerSubgroup
    (z : localization vK w) :
    Subgroup (absoluteValueDecompositionGroup K w.1)
theorem

mem_algebraicLocalizationStabilizerSubgroup_iff

L144 ↗
ClassFieldTower.Martinet.Shafarevich.mem_algebraicLocalizationStabilizerSubgroup_iff
Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
theorem mem_algebraicLocalizationStabilizerSubgroup_iff
    (z : localization vK w) (sigma : absoluteValueDecompositionGroup K w.1) :
    sigma ∈ algebraicLocalizationStabilizerSubgroup vK hvK w z ↔
      decompositionGroupToAlgebraicLocalizationMonoidHom vK hvK w sigma z = z
theorem

decompositionGroupToAlgebraicLocalization_stabilizer_isOpen

L152 ↗
ClassFieldTower.Martinet.Shafarevich.decompositionGroupToAlgebraicLocalization_stabilizer_isOpen
Documentation

The stabilizer of one algebraic-localization element has open preimage in the decomposition group.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
theorem decompositionGroupToAlgebraicLocalization_stabilizer_isOpen
    (z : localization vK w) :
    IsOpen (algebraicLocalizationStabilizerSubgroup vK hvK w z :
      Set (absoluteValueDecompositionGroup K w.1))
theorem

decompositionGroupToAlgebraicLocalization_fixingSubgroup_mem_nhds

L165 ↗
ClassFieldTower.Martinet.Shafarevich.decompositionGroupToAlgebraicLocalization_fixingSubgroup_mem_nhds
Documentation

The preimage of a finite-stage fixing subgroup is a neighborhood of the identity in the decomposition group.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
theorem decompositionGroupToAlgebraicLocalization_fixingSubgroup_mem_nhds
    (E : IntermediateField vK.Completion (localization vK w))
    [FiniteDimensional vK.Completion E] :
    {sigma : absoluteValueDecompositionGroup K w.1 |
        decompositionGroupToAlgebraicLocalizationMonoidHom vK hvK w sigma ∈
          E.fixingSubgroup} ∈ 𝓝 1
theorem

decompositionGroupToAlgebraicLocalization_continuous

L194 ↗
ClassFieldTower.Martinet.Shafarevich.decompositionGroupToAlgebraicLocalization_continuous
Documentation

The decomposition--localization comparison is continuous for the two Krull topologies.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
theorem decompositionGroupToAlgebraicLocalization_continuous :
    Continuous (decompositionGroupEquivAlgebraicLocalizationAut vK hvK w)
def

decompositionGroupContinuousMulEquivAlgebraicLocalizationAut

L213 ↗
ClassFieldTower.Martinet.Shafarevich.decompositionGroupContinuousMulEquivAlgebraicLocalizationAut
Documentation

The decomposition group and the algebraic-localization Galois group are canonically isomorphic as topological groups.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open scoped Topology
universe u v
section GeneralLocalization
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
variable (vK : AbsoluteValue K ℝ) (hvK : vK.IsNontrivial)
variable (w : AbsoluteValueExtension vK L)
local instance generalLocalizationBaseAlgebra : Algebra K w.1.Completion :=
  AbsoluteValue.extensionCompletionAlgebra (K := K) w.1
local instance generalLocalizationBaseSMul : SMul K w.1.Completion :=
  (AbsoluteValue.extensionCompletionAlgebra (K := K) w.1).toSMul
local instance generalLocalizationCompletionAlgebra :
    Algebra vK.Completion w.1.Completion :=
  AbsoluteValue.completionAlgebra vK w.1 w.2
Lean source · statement
def decompositionGroupContinuousMulEquivAlgebraicLocalizationAut :
    absoluteValueDecompositionGroup K w.1 ≃ₜ*
      (localization vK w ≃ₐ[vK.Completion] localization vK w)

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