The stable general linear group and algebraic K₁

For a possibly noncommutative ring A and m ≤ n, stabilization places an invertible m × m matrix u in the upper left corner of an n × n matrix and fills the rest with the identity, u ↦ u ⊕ 1. These homomorphisms form a directed system of groups indexed by ℕ, and the stable general linear group GL_∞(A) is its direct limit. The stable elementary subgroup E_∞(A) is the union of the images of the elementary subgroups E n A.

The finite-size relations of TauCeti.LinearAlgebra.Matrix.GeneralLinearGroup.Elementary become exact statements in the limit: E_∞(A) is a normal subgroup of GL_∞(A), and it is the commutator subgroup of GL_∞(A). Hence algebraic K₁(A) = GL_∞(A) / E_∞(A) is an abelian group, the abelianization of GL_∞(A). Homomorphisms on invertible matrices which are compatible with stabilization and take values in an abelian group, such as Connes' odd pairing with cyclic cohomology, factor through it. A ring homomorphism, applied to the entries of invertible matrices, induces a homomorphism of algebraic K₁, functorially.

Main definitions

• TauCeti.stabilizeGL: the stabilization homomorphism GL (Fin m) A →* GL (Fin n) A, u ↦ u ⊕ 1, for m ≤ n.
• TauCeti.StableGeneralLinearGroup: the direct limit GL_∞(A) of the groups GL (Fin n) A.
• TauCeti.StableGeneralLinearGroup.of: the canonical homomorphism GL (Fin n) A →* GL_∞(A).
• TauCeti.StableGeneralLinearGroup.lift: the universal property of GL_∞(A), for families of homomorphisms compatible with stabilization.
• TauCeti.StableGeneralLinearGroup.elementarySubgroup: the stable elementary subgroup E_∞(A).
• TauCeti.AlgebraicK1: algebraic K₁(A), the abelianization of GL_∞(A).
• TauCeti.AlgebraicK1.mk: the class in K₁(A) of an invertible matrix.
• TauCeti.AlgebraicK1.lift: the universal property of K₁(A), for families of homomorphisms to a commutative group compatible with stabilization.
• TauCeti.AlgebraicK1.quotientElementarySubgroupEquiv: GL_∞(A) / E_∞(A) ≃* K₁(A).
• TauCeti.AlgebraicK1.map: the homomorphism K₁(A) →* K₁(B) induced by a ring homomorphism.

Main results

• TauCeti.coe_stabilizeGL_apply: the entries of a stabilized matrix.
• TauCeti.StableGeneralLinearGroup.mem_elementarySubgroup_iff: an element of GL_∞(A) is stably elementary exactly when it is represented by an elementary matrix of some size.
• TauCeti.StableGeneralLinearGroup.elementarySubgroup_normal: E_∞(A) is normal.
• TauCeti.StableGeneralLinearGroup.elementarySubgroup_eq_commutator: E_∞(A) is the commutator subgroup of GL_∞(A).
• TauCeti.AlgebraicK1.mk_eq_one_iff: an invertible matrix has trivial class in K₁(A) exactly when some stabilization of it is elementary.
• TauCeti.AlgebraicK1.map_id, TauCeti.AlgebraicK1.map_comp, TauCeti.AlgebraicK1.map_map: functoriality of algebraic K₁.

References

• J. Milnor, Introduction to Algebraic K-Theory, Annals of Mathematics Studies 72 (1971), §3, Lemma 3.1 (Whitehead) and the definition of K₁ following it.
• J. Rosenberg, Algebraic K-Theory and Its Applications, GTM 147 (1994), §2.1, Definition 2.1.1 and Proposition 2.1.4.

Stabilization

def TauCeti.stabilizeGL (A : Type u_1) [Ring A] {m n : ℕ} (h : m ≤ n) : GL (Fin m) A →* GL (Fin n) A

The stabilization homomorphism u ↦ u ⊕ 1 from GL (Fin m) A to GL (Fin n) A, for m ≤ n: the image of u agrees with u on the first m rows and columns and with the identity matrix elsewhere.

theorem TauCeti.coe_stabilizeGL_apply {A : Type u_1} [Ring A] {m n : ℕ} (h : m ≤ n) (u : GL (Fin m) A) (i j : Fin n) : ↑((stabilizeGL A h) u) i j = if hij : ↑i < m ∧ ↑j < m then ↑u ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩ else 1 i j

The entries of a stabilized matrix: those of u in the first m rows and columns, and those of the identity matrix elsewhere.

@[simp]

theorem TauCeti.stabilizeGL_refl {A : Type u_1} [Ring A] (n : ℕ) : stabilizeGL A ⋯ = MonoidHom.id (GL (Fin n) A)

Stabilization to the same size is the identity.

@[simp]

theorem TauCeti.stabilizeGL_stabilizeGL {A : Type u_1} [Ring A] {k m n : ℕ} (hkm : k ≤ m) (hmn : m ≤ n) (u : GL (Fin k) A) : (stabilizeGL A hmn) ((stabilizeGL A hkm) u) = (stabilizeGL A ⋯) u

Stabilizations compose.

theorem TauCeti.stabilizeGL_injective {A : Type u_1} [Ring A] {m n : ℕ} (h : m ≤ n) : Function.Injective ⇑(stabilizeGL A h)

Stabilization is injective: the stabilized matrix contains u as its upper left block.

theorem TauCeti.stabilizeGL_eq_reindexGL_fromBlocksGL {A : Type u_1} [Ring A] (m k : ℕ) (u : GL (Fin m) A) : (stabilizeGL A ⋯) u = (finSumFinEquiv.reindexGL A) (fromBlocksGL (u, 1))

Stabilizing u to size m + k is the block diagonal matrix u ⊕ 1, reindexed along Fin m ⊕ Fin k ≃ Fin (m + k).

theorem TauCeti.stabilizeGL_transvectionUnit {A : Type u_1} [Ring A] {m n : ℕ} (h : m ≤ n) {i j : Fin m} (hij : i ≠ j) (a : A) : (stabilizeGL A h) (transvectionUnit hij a) = transvectionUnit ⋯ a

Stabilization sends an elementary matrix to the elementary matrix with the same parameter at the same pair of indices.

theorem TauCeti.map_stabilizeGL_elementarySubgroup_le {A : Type u_1} [Ring A] {m n : ℕ} (h : m ≤ n) : Subgroup.map (stabilizeGL A h) (elementarySubgroup (Fin m) A) ≤ elementarySubgroup (Fin n) A

Stabilization maps the elementary subgroup into the elementary subgroup.

instance TauCeti.instDirectedSystemNatGeneralLinearGroupFinCoeMonoidHomStabilizeGL {A : Type u_1} [Ring A] : DirectedSystem (fun (n : ℕ) => GL (Fin n) A) fun (x x_1 : ℕ) (h : x ≤ x_1) => ⇑(stabilizeGL A h)

The stabilizations form a directed system of groups.

@[reducible, inline]

abbrev TauCeti.StableGeneralLinearGroup (A : Type u_1) [Ring A] : Type u_1

The stable general linear group GL_∞(A): the direct limit of the groups GL (Fin n) A along the stabilizations u ↦ u ⊕ 1.

def TauCeti.StableGeneralLinearGroup.of (A : Type u_1) [Ring A] (n : ℕ) : GL (Fin n) A →* StableGeneralLinearGroup A

The canonical homomorphism from GL (Fin n) A to the stable general linear group.

@[simp]

theorem TauCeti.StableGeneralLinearGroup.of_stabilizeGL {A : Type u_1} [Ring A] {m n : ℕ} (h : m ≤ n) (u : GL (Fin m) A) : (of A n) ((stabilizeGL A h) u) = (of A m) u

The canonical homomorphisms are compatible with stabilization.

theorem TauCeti.StableGeneralLinearGroup.of_comp_stabilizeGL {A : Type u_1} [Ring A] {m n : ℕ} (h : m ≤ n) : (of A n).comp (stabilizeGL A h) = of A m

The canonical homomorphisms are compatible with stabilization.

theorem TauCeti.StableGeneralLinearGroup.of_injective {A : Type u_1} [Ring A] (n : ℕ) : Function.Injective ⇑(of A n)

The canonical homomorphisms are injective.

theorem TauCeti.StableGeneralLinearGroup.exists_of {A : Type u_1} [Ring A] (x : StableGeneralLinearGroup A) : ∃ (n : ℕ) (u : GL (Fin n) A), (of A n) u = x

Every element of the stable general linear group comes from an invertible matrix of some size.

theorem TauCeti.StableGeneralLinearGroup.exists_of₂ {A : Type u_1} [Ring A] (x y : StableGeneralLinearGroup A) : ∃ (n : ℕ) (u : GL (Fin n) A) (v : GL (Fin n) A), (of A n) u = x ∧ (of A n) v = y

Any two elements of the stable general linear group come from invertible matrices of a common size.

theorem TauCeti.StableGeneralLinearGroup.hom_ext {A : Type u_1} [Ring A] {G : Type u_2} [Monoid G] {f g : StableGeneralLinearGroup A →* G} (h : ∀ (n : ℕ), f.comp (of A n) = g.comp (of A n)) : f = g

Homomorphisms out of the stable general linear group agree when they agree on each GL (Fin n) A.

theorem TauCeti.StableGeneralLinearGroup.hom_ext_iff {A : Type u_1} [Ring A] {G : Type u_2} [Monoid G] {f g : StableGeneralLinearGroup A →* G} : f = g ↔ ∀ (n : ℕ), f.comp (of A n) = g.comp (of A n)

def TauCeti.StableGeneralLinearGroup.lift {A : Type u_1} [Ring A] {G : Type u_2} [Monoid G] (f : (n : ℕ) → GL (Fin n) A →* G) (hf : ∀ (m n : ℕ) (h : m ≤ n) (u : GL (Fin m) A), (f n) ((stabilizeGL A h) u) = (f m) u) : StableGeneralLinearGroup A →* G

The universal property of GL_∞(A): a family of homomorphisms out of the groups GL (Fin n) A which is compatible with stabilization induces a homomorphism out of the stable general linear group.

@[simp]

theorem TauCeti.StableGeneralLinearGroup.lift_of {A : Type u_1} [Ring A] {G : Type u_2} [Monoid G] (f : (n : ℕ) → GL (Fin n) A →* G) (hf : ∀ (m n : ℕ) (h : m ≤ n) (u : GL (Fin m) A), (f n) ((stabilizeGL A h) u) = (f m) u) (n : ℕ) (u : GL (Fin n) A) : (lift f hf) ((of A n) u) = (f n) u

The homomorphism induced by a compatible family restricts to the family.

The stable elementary subgroup

noncomputable def TauCeti.StableGeneralLinearGroup.elementarySubgroup (A : Type u_1) [Ring A] : Subgroup (StableGeneralLinearGroup A)

The stable elementary subgroup E_∞(A) of GL_∞(A): the union of the images of the elementary subgroups of GL (Fin n) A.

theorem TauCeti.StableGeneralLinearGroup.mem_elementarySubgroup_iff {A : Type u_1} [Ring A] {x : StableGeneralLinearGroup A} : x ∈ elementarySubgroup A ↔ ∃ (n : ℕ), ∃ u ∈ TauCeti.elementarySubgroup (Fin n) A, (of A n) u = x

An element of GL_∞(A) is stably elementary exactly when it comes from an elementary matrix of some size.

theorem TauCeti.StableGeneralLinearGroup.of_mem_elementarySubgroup {A : Type u_1} [Ring A] {n : ℕ} {u : GL (Fin n) A} (hu : u ∈ TauCeti.elementarySubgroup (Fin n) A) : (of A n) u ∈ elementarySubgroup A

Elementary matrices are stably elementary.

theorem TauCeti.StableGeneralLinearGroup.of_mem_elementarySubgroup_iff {A : Type u_1} [Ring A] {n : ℕ} {u : GL (Fin n) A} : (of A n) u ∈ elementarySubgroup A ↔ ∃ (k : ℕ) (h : n ≤ k), (stabilizeGL A h) u ∈ TauCeti.elementarySubgroup (Fin k) A

An invertible matrix is stably elementary exactly when some stabilization of it is elementary.

instance TauCeti.StableGeneralLinearGroup.elementarySubgroup_normal {A : Type u_1} [Ring A] : (elementarySubgroup A).Normal

The stable elementary subgroup is normal. This is Whitehead's lemma in the limit: a conjugate g e g⁻¹ becomes elementary after stabilization.

theorem TauCeti.StableGeneralLinearGroup.commutator_le_elementarySubgroup {A : Type u_1} [Ring A] : commutator (StableGeneralLinearGroup A) ≤ elementarySubgroup A

The commutator subgroup of GL_∞(A) is contained in the stable elementary subgroup.

theorem TauCeti.StableGeneralLinearGroup.elementarySubgroup_eq_commutator {A : Type u_1} [Ring A] : elementarySubgroup A = commutator (StableGeneralLinearGroup A)

The stable elementary subgroup is the commutator subgroup of GL_∞(A): every commutator is stably elementary, and every elementary matrix of size at least three is a commutator of elementary matrices.

Algebraic K₁

@[reducible, inline]

abbrev TauCeti.AlgebraicK1 (A : Type u_1) [Ring A] : Type u_1

Algebraic K₁ of a ring A: the quotient GL_∞(A) / E_∞(A) of the stable general linear group by the stable elementary subgroup. Since E_∞(A) is the commutator subgroup (TauCeti.StableGeneralLinearGroup.elementarySubgroup_eq_commutator), this is the abelianization of GL_∞(A), and it is defined as such.

noncomputable def TauCeti.AlgebraicK1.mk (A : Type u_1) [Ring A] (n : ℕ) : GL (Fin n) A →* AlgebraicK1 A

The class in algebraic K₁ of an invertible matrix.

@[simp]

theorem TauCeti.AlgebraicK1.mk_stabilizeGL {A : Type u_1} [Ring A] {m n : ℕ} (h : m ≤ n) (u : GL (Fin m) A) : (mk A n) ((stabilizeGL A h) u) = (mk A m) u

The class of an invertible matrix is unchanged by stabilization.

theorem TauCeti.AlgebraicK1.exists_mk {A : Type u_1} [Ring A] (x : AlgebraicK1 A) : ∃ (n : ℕ) (u : GL (Fin n) A), (mk A n) u = x

Every class in algebraic K₁ is the class of an invertible matrix of some size.

theorem TauCeti.AlgebraicK1.ker_of {A : Type u_1} [Ring A] : Abelianization.of.ker = StableGeneralLinearGroup.elementarySubgroup A

The kernel of the projection GL_∞(A) → K₁(A) is the stable elementary subgroup.

theorem TauCeti.AlgebraicK1.mk_eq_one_iff {A : Type u_1} [Ring A] {n : ℕ} {u : GL (Fin n) A} : (mk A n) u = 1 ↔ ∃ (k : ℕ) (h : n ≤ k), (stabilizeGL A h) u ∈ elementarySubgroup (Fin k) A

The class of an invertible matrix in algebraic K₁ is trivial exactly when some stabilization of the matrix is elementary.

theorem TauCeti.AlgebraicK1.mk_eq_mk_iff {A : Type u_1} [Ring A] {n : ℕ} {u v : GL (Fin n) A} : (mk A n) u = (mk A n) v ↔ ∃ (k : ℕ) (h : n ≤ k), (stabilizeGL A h) (u⁻¹ * v) ∈ elementarySubgroup (Fin k) A

Two invertible matrices of the same size have the same class in algebraic K₁ exactly when they agree modulo elementary matrices after some stabilization.

noncomputable def TauCeti.AlgebraicK1.quotientElementarySubgroupEquiv (A : Type u_1) [Ring A] : StableGeneralLinearGroup A ⧸ StableGeneralLinearGroup.elementarySubgroup A ≃* AlgebraicK1 A

Algebraic K₁ is the quotient of GL_∞(A) by the stable elementary subgroup.

@[simp]

theorem TauCeti.AlgebraicK1.quotientElementarySubgroupEquiv_mk {A : Type u_1} [Ring A] (x : StableGeneralLinearGroup A) : (quotientElementarySubgroupEquiv A) ↑x = Abelianization.of x

The identification of GL_∞(A) / E_∞(A) with algebraic K₁ respects the projections.

theorem TauCeti.AlgebraicK1.hom_ext {A : Type u_1} [Ring A] {G : Type u_2} [Monoid G] {f g : AlgebraicK1 A →* G} (h : ∀ (n : ℕ), f.comp (mk A n) = g.comp (mk A n)) : f = g

Homomorphisms out of algebraic K₁ agree when they agree on the classes of invertible matrices of each size.

theorem TauCeti.AlgebraicK1.hom_ext_iff {A : Type u_1} [Ring A] {G : Type u_2} [Monoid G] {f g : AlgebraicK1 A →* G} : f = g ↔ ∀ (n : ℕ), f.comp (mk A n) = g.comp (mk A n)

noncomputable def TauCeti.AlgebraicK1.lift {A : Type u_1} [Ring A] {G : Type u_2} [CommGroup G] (f : (n : ℕ) → GL (Fin n) A →* G) (hf : ∀ (m n : ℕ) (h : m ≤ n) (u : GL (Fin m) A), (f n) ((stabilizeGL A h) u) = (f m) u) : AlgebraicK1 A →* G

The universal property of algebraic K₁: a family of homomorphisms from the groups GL (Fin n) A to a commutative group which is compatible with stabilization induces a homomorphism out of algebraic K₁.

@[simp]

theorem TauCeti.AlgebraicK1.lift_mk {A : Type u_1} [Ring A] {G : Type u_2} [CommGroup G] (f : (n : ℕ) → GL (Fin n) A →* G) (hf : ∀ (m n : ℕ) (h : m ≤ n) (u : GL (Fin m) A), (f n) ((stabilizeGL A h) u) = (f m) u) (n : ℕ) (u : GL (Fin n) A) : (lift f hf) ((mk A n) u) = (f n) u

The homomorphism induced by a compatible family sends the class of an invertible matrix to its value under the family.

Functoriality

theorem TauCeti.stabilizeGL_map {A : Type u_1} [Ring A] {B : Type u_2} [Ring B] {m n : ℕ} (h : m ≤ n) (f : A →+* B) (u : GL (Fin m) A) : (stabilizeGL B h) ((Units.map ↑f.mapMatrix) u) = (Units.map ↑f.mapMatrix) ((stabilizeGL A h) u)

Stabilization commutes with applying a ring homomorphism to the entries of an invertible matrix.

noncomputable def TauCeti.AlgebraicK1.map {A : Type u_1} [Ring A] {B : Type u_2} [Ring B] (f : A →+* B) : AlgebraicK1 A →* AlgebraicK1 B

The homomorphism of algebraic K₁ induced by a ring homomorphism f : A →+* B, applying f to the entries of invertible matrices.

@[simp]

theorem TauCeti.AlgebraicK1.map_mk {A : Type u_1} [Ring A] {B : Type u_2} [Ring B] (f : A →+* B) (n : ℕ) (u : GL (Fin n) A) : (map f) ((mk A n) u) = (mk B n) ((Units.map ↑f.mapMatrix) u)

The induced homomorphism of algebraic K₁ sends the class of an invertible matrix to the class of the matrix obtained by applying the ring homomorphism to its entries.

@[simp]

theorem TauCeti.AlgebraicK1.map_id {A : Type u_1} [Ring A] : map (RingHom.id A) = MonoidHom.id (AlgebraicK1 A)

The identity ring homomorphism induces the identity of algebraic K₁.

theorem TauCeti.AlgebraicK1.map_comp {A : Type u_1} [Ring A] {B : Type u_2} {C : Type u_3} [Ring B] [Ring C] (f : A →+* B) (g : B →+* C) : map (g.comp f) = (map g).comp (map f)

Algebraic K₁ is functorial.

@[simp]

theorem TauCeti.AlgebraicK1.map_map {A : Type u_1} [Ring A] {B : Type u_2} {C : Type u_3} [Ring B] [Ring C] (f : A →+* B) (g : B →+* C) (x : AlgebraicK1 A) : (map g) ((map f) x) = (map (g.comp f)) x

Applying the homomorphisms of algebraic K₁ induced by f and then g is applying the one induced by g.comp f.