Documentation

TauCeti.RingTheory.Huber.Matrix

Nakayama for a matrix with topologically nilpotent entries #

Over a complete nonarchimedean ring, 1 - B is invertible as soon as every entry of B is topologically nilpotent, and consequently a family satisfying yᵢ = ∑ⱼ Bᵢⱼ • yⱼ vanishes.

The vanishing argument is split from its topological input. Once 1 - B is a unit the conclusion is pure algebra, and TauCeti.eq_zero_of_isUnit_one_sub_of_forall_eq_sum_smul states it that way in TauCeti.LinearAlgebra.Matrix.Module, where it needs no ring theory at all: the module P carries no topology, and A need not be commutative, which is what lets it be applied where P is an abstract subquotient. This file supplies only the topological input.

Main results #

References #

Provenance #

AINTLIB (github.com/CBirkbeck/AINTLIB @ 37bbdaeb9, Apache-2.0) has all three of the topological statements in projects/AdicSpaces/Adic spaces/Bounded.lean — IsTopologicallyNilpotent.one_sub_det_one_sub_matrix (:666), IsTopologicallyNilpotent.isUnit_one_sub_matrix (:704) and eq_zero_of_forall_eq_sum_topNilp_smul (:740) — and takes the same route: lift to the power-bounded subring, reduce modulo the topologically nilpotent ideal, apply RingHom.map_det, then Matrix.isUnit_iff_isUnit_det. This module was written against this repository's own API and compared afterwards; since the routes coincide it should be read as a re-derivation of that argument rather than an independent one. Nothing was copied: the names differ throughout, the hypotheses here are the plain nonarchimedean bundle rather than AINTLIB's section variables, the vanishing step goes through Mathlib's Matrix.Module action, and the algebraic core is split out, which AINTLIB does not do.

The determinant modulo topologically nilpotent entries #

source
theorem TauCeti.Huber.isTopologicallyNilpotent_one_sub_det_one_sub {A : Type u_1} [CommRing A] [TopologicalSpace A] [NonarchimedeanRing A] {n : Type u_2} [Fintype n] [DecidableEq n] {B : Matrix n n A} (hB : ∀ (i j : n), IsTopologicallyNilpotent (B i j)) :
IsTopologicallyNilpotent (1 - (1 - B).det)

The determinant of 1 - B is 1 up to a topologically nilpotent error. Every entry of B lies in the ideal A°° of A°, so 1 - B reduces to the identity modulo that ideal and its determinant reduces to 1.

Invertibility, and Nakayama #

source
theorem TauCeti.Huber.isUnit_one_sub_of_isTopologicallyNilpotent_entries {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsUniformAddGroup A] [NonarchimedeanRing A] {n : Type u_2} [Fintype n] [DecidableEq n] {B : Matrix n n A} (hB : ∀ (i j : n), IsTopologicallyNilpotent (B i j)) :
IsUnit (1 - B)

1 - B is invertible when every entry of B is topologically nilpotent. The determinant is 1 minus a topologically nilpotent element, hence a unit by the geometric series, and a square matrix over a commutative ring is a unit exactly when its determinant is.

source
theorem TauCeti.Huber.eq_zero_of_isTopologicallyNilpotent_entries_of_forall_eq_sum_smul {A : Type u_1} [CommRing A] [UniformSpace A] [T2Space A] [CompleteSpace A] [IsUniformAddGroup A] [NonarchimedeanRing A] {n : Type u_2} [Fintype n] {P : Type u_3} [AddCommGroup P] [Module A P] {B : Matrix n n A} (hB : ∀ (i j : n), IsTopologicallyNilpotent (B i j)) {y : n → P} (hy : ∀ (i : n), y i = ∑ j : n, B i j • y j) :
y = 0

Nakayama for topologically nilpotent entries. If every entry of B is topologically nilpotent and yᵢ = ∑ⱼ Bᵢⱼ • yⱼ for every i, then the whole family vanishes. This is TauCeti.eq_zero_of_isUnit_one_sub_of_forall_eq_sum_smul with its hypothesis discharged; a consumer wanting a single coordinate applies congrFun.