NYLL
Module

AdicPerfect.lean

Nyll.Yamaguchi26SolvableCoverings.Representations.AdicPerfect
6 declarations indexed from sourceView source ↗

Module documentation

完全な位相群の合同表現は自明

I 進位相を持つ可換環 A が I 進分離的であるとする。 交換子部分群が稠密な位相群 G から GLₙ(A) への連続表現が I を法として 自明なら、表現自体が自明である。

証明は合同核の pro-p 性を仮定せず、行列の差を直接計算する。 I^r を法として単位行列となる二つの行列は、r ≥ 1 のとき I^(r+1) を法として 可換である。これは二つの差の積の成分が I^(2r) ⊆ I^(r+1) に入るためである。 したがって各段階の剰余表現は交換子部分群を消し、連続性と稠密性により全体を消す。 帰納的に全ての I の冪を法として自明となり、分離性から結論が従う。

系2.6では I は極大イデアルであり、完備性からこの分離性が得られる。 この補助定理自体には剰余体の有限性・Noether 性・G のコンパクト性は不要である。

Imports12
  • Mathlib.Algebra.Ring.Commute
  • Mathlib.GroupTheory.Commutator.Basic
  • Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
  • Mathlib.RingTheory.AdicCompletion.Basic
  • Mathlib.RingTheory.Ideal.Operations
  • Mathlib.RingTheory.Ideal.Quotient.Defs
  • Mathlib.Topology.Algebra.ContinuousMonoidHom
  • Mathlib.Topology.Algebra.Group.Subgroup
  • Mathlib.Topology.Algebra.Group.Matrix
  • Mathlib.Topology.Algebra.Group.Units
  • Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
  • Mathlib.Topology.Instances.Matrix
Imported by2

Declarations

theorem

gl_map_quotient_eq_one_iff

L43 ↗
Yamaguchi26SolvableCoverings.gl_map_quotient_eq_one_iff
Source context 3 commands

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

noncomputable section
open scoped BigOperators commutatorElement
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem gl_map_quotient_eq_one_iff
    {A ι : Type*} [CommRing A] [Fintype ι] [DecidableEq ι]
    (I : Ideal A) (x : Matrix.GeneralLinearGroup ι A) :
    Matrix.GeneralLinearGroup.map (Ideal.Quotient.mk I) x = 1 ↔
      ∀ i j : ι, ((x : Matrix ι ι A) - 1) i j ∈ I
theorem

matrix_error_product_eq_zero_mod_succ

L65 ↗
Yamaguchi26SolvableCoverings.matrix_error_product_eq_zero_mod_succ
Source context 3 commands

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

noncomputable section
open scoped BigOperators commutatorElement
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem matrix_error_product_eq_zero_mod_succ
    {A ι : Type*} [CommRing A] [Fintype ι] [DecidableEq ι]
    (I : Ideal A) (r : ℕ) (hr : 1 ≤ r)
    (M N : Matrix ι ι A)
    (hM : ∀ i j, M i j ∈ I ^ r) (hN : ∀ i j, N i j ∈ I ^ r) :
    RingHom.mapMatrix (Ideal.Quotient.mk (I ^ (r + 1))) (M * N) = 0
theorem

gl_reductions_commute_of_congruent_one

L86 ↗
Yamaguchi26SolvableCoverings.gl_reductions_commute_of_congruent_one
Documentation

Two matrices congruent to the identity modulo I^r commute modulo I^(r+1) when r ≥ 1; both products of their error matrices vanish there.

Source context 3 commands

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

noncomputable section
open scoped BigOperators commutatorElement
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem gl_reductions_commute_of_congruent_one
    {A ι : Type*} [CommRing A] [Fintype ι] [DecidableEq ι]
    (I : Ideal A) (r : ℕ) (hr : 1 ≤ r)
    (x y : Matrix.GeneralLinearGroup ι A)
    (hx : Matrix.GeneralLinearGroup.map (Ideal.Quotient.mk (I ^ r)) x = 1)
    (hy : Matrix.GeneralLinearGroup.map (Ideal.Quotient.mk (I ^ r)) y = 1) :
    Commute
      (Matrix.GeneralLinearGroup.map (Ideal.Quotient.mk (I ^ (r + 1))) x)
      (Matrix.GeneralLinearGroup.map (Ideal.Quotient.mk (I ^ (r + 1))) y)
theorem

continuous_quotient_of_isOpen

L119 ↗
Yamaguchi26SolvableCoverings.continuous_quotient_of_isOpen
Source context 3 commands

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

noncomputable section
open scoped BigOperators commutatorElement
namespace Yamaguchi26SolvableCoverings
Lean source · full declaration
theorem continuous_quotient_of_isOpen
    {A : Type*} [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    (I : Ideal A) (hI : IsOpen (I : Set A)) :
    letI : TopologicalSpace (A ⧸ I) := ⊥
    Continuous (Ideal.Quotient.mk I) := by
  let : TopologicalSpace (A ⧸ I) := ⊥
  have : DiscreteTopology (A ⧸ I) := discreteTopology_bot _
  rw [continuous_discrete_rng]
  intro y
  rcases Ideal.Quotient.mk_surjective y with ⟨x, hx⟩
  have hpreimage : Ideal.Quotient.mk I ⁻¹' ({y} : Set (A ⧸ I)) =
      (fun z : A => z - x) ⁻¹' (I : Set A) := by
    ext z
    change Ideal.Quotient.mk I z = y ↔ z - x ∈ I
    rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, hx, sub_eq_zero]
  rw [hpreimage]
  exact hI.preimage (continuous_id.sub continuous_const)
theorem

representation_eq_one_of_dense_commutator_of_commuting_image

L137 ↗
Yamaguchi26SolvableCoverings.representation_eq_one_of_dense_commutator_of_commuting_image
Source context 3 commands

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

noncomputable section
open scoped BigOperators commutatorElement
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem representation_eq_one_of_dense_commutator_of_commuting_image
    {G H : Type*} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [Group H] [TopologicalSpace H] [T2Space H]
    (hperfect : (commutator G).topologicalClosure = ⊤)
    (ρ : G →ₜ* H) (hcomm : ∀ x y : G, Commute (ρ x) (ρ y)) :
    ∀ g : G, ρ g = 1
theorem

adic_representation_eq_one_of_dense_commutator

L161 ↗
Yamaguchi26SolvableCoverings.adic_representation_eq_one_of_dense_commutator
Documentation

A continuous representation of a group with dense commutator subgroup into matrices over a separated adic ring is trivial if its reduction modulo the defining ideal is trivial. The congruence filtration is proved directly.

Source context 3 commands

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

noncomputable section
open scoped BigOperators commutatorElement
namespace Yamaguchi26SolvableCoverings
Lean source · statement
theorem adic_representation_eq_one_of_dense_commutator
    {G A ι : Type*}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CommRing A] [TopologicalSpace A] [IsTopologicalRing A]
    [Fintype ι] [DecidableEq ι]
    (I : Ideal A) [IsHausdorff I A] (hAdic : IsAdic I)
    (hperfect : (commutator G).topologicalClosure = ⊤)
    (ρ : G →ₜ* Matrix.GeneralLinearGroup ι A)
    (hmod : ∀ g : G, Matrix.GeneralLinearGroup.map (Ideal.Quotient.mk I) (ρ g) = 1) :
    ∀ g : G, ρ g = 1

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