Relative algebraic K₁ of a nonunital algebra

Let A be a possibly nonunital algebra over a commutative ring R, and A⁺ = Unitization R A its forced unitization, used even when A already has a unit. The augmentation A⁺ → R, (r, a) ↦ r, induces a homomorphism K₁(A⁺) → K₁(R), and the relative K₁ of A is its kernel. This is the K₁-group of a nonunital algebra; for a unital A it is computed with the forced unitization all the same. The scalar inclusion R → A⁺ splits the augmentation, so every class of A⁺ is the product of its relative part and the class of a scalar matrix.

Invertible matrices over A⁺ whose scalar part is the identity, that is matrices 1 + a with entries of a in A, have relative classes. A homomorphism of nonunital algebras induces a homomorphism of relative K₁ through the induced map of forced unitizations, which preserves the augmentation.

Relative K₁ is the group paired with the relative cyclic cohomology of A by Connes' odd pairing (TauCeti.relativeAlgebraicK1.oddPairing).

Main definitions

• TauCeti.relativeAlgebraicK1: the kernel of K₁(A⁺) → K₁(R).
• TauCeti.relativeAlgebraicK1.projection: the projection of K₁(A⁺) onto relative K₁ along the classes of scalar matrices.
• TauCeti.relativeAlgebraicK1.map: the homomorphism induced by a homomorphism of nonunital algebras.

Main results

• TauCeti.AlgebraicK1.mk_mem_relativeAlgebraicK1: an invertible matrix over A⁺ with identity scalar part has a relative class.
• TauCeti.relativeAlgebraicK1.projection_coe, TauCeti.relativeAlgebraicK1.projection_map_algebraMap: the projection is the identity on relative classes and kills the classes of scalar matrices.
• TauCeti.relativeAlgebraicK1.coe_projection_mul_map_algebraMap: every class of A⁺ is its relative part times the class of a scalar matrix.
• TauCeti.relativeAlgebraicK1.map_projection: the projection is natural.
• TauCeti.relativeAlgebraicK1.map_id, TauCeti.relativeAlgebraicK1.map_comp: functoriality.

References

• J. Rosenberg, Algebraic K-Theory and Its Applications, GTM 147 (1994), Chapters 1 and 2, for K-groups of nonunital rings through their unitization.
• A. Connes, Noncommutative Geometry, Chapter III, §3, for the K-theory of a nonunital algebra as a kernel on its unitization in the pairing with cyclic cohomology.

noncomputable def TauCeti.relativeAlgebraicK1 (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : Subgroup (AlgebraicK1 (Unitization R A))

The relative algebraic K₁ of a possibly nonunital algebra A: the kernel of the homomorphism K₁(A⁺) → K₁(R) induced by the augmentation of the forced unitization A⁺ = Unitization R A.

@[simp]

theorem TauCeti.mem_relativeAlgebraicK1_iff {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {x : AlgebraicK1 (Unitization R A)} : x ∈ relativeAlgebraicK1 R A ↔ (AlgebraicK1.map ↑(Unitization.fstHom R A)) x = 1

A class of A⁺ is relative exactly when the augmentation sends it to the trivial class.

theorem TauCeti.AlgebraicK1.mk_mem_relativeAlgebraicK1 {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {n : ℕ} {u : GL (Fin n) (Unitization R A)} (hu : (↑(Unitization.fstHom R A)).mapMatrix ↑u = 1) : (mk (Unitization R A) n) u ∈ relativeAlgebraicK1 R A

An invertible matrix over A⁺ whose scalar part is the identity matrix has a relative class.

theorem TauCeti.AlgebraicK1.map_fstHom_map_algebraMap {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : AlgebraicK1 R) : (map ↑(Unitization.fstHom R A)) ((map (algebraMap R (Unitization R A))) x) = x

The augmentation is a left inverse of the scalar inclusion on algebraic K₁.

noncomputable def TauCeti.relativeAlgebraicK1.projection (R : Type u_1) (A : Type u_2) [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : AlgebraicK1 (Unitization R A) →* ↥(relativeAlgebraicK1 R A)

The projection of K₁(A⁺) onto relative K₁ along the classes of scalar matrices, x ↦ x · s(ε(x))⁻¹, where ε is induced by the augmentation and s by the scalar inclusion.

theorem TauCeti.relativeAlgebraicK1.coe_projection_apply {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : AlgebraicK1 (Unitization R A)) : ↑((projection R A) x) = x * ((AlgebraicK1.map (algebraMap R (Unitization R A))) ((AlgebraicK1.map ↑(Unitization.fstHom R A)) x))⁻¹

The relative part of a class x of A⁺ is x · s(ε(x))⁻¹.

@[simp]

theorem TauCeti.relativeAlgebraicK1.projection_coe {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : ↥(relativeAlgebraicK1 R A)) : (projection R A) ↑x = x

The projection is the identity on relative classes.

@[simp]

theorem TauCeti.relativeAlgebraicK1.projection_map_algebraMap {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (y : AlgebraicK1 R) : (projection R A) ((AlgebraicK1.map (algebraMap R (Unitization R A))) y) = 1

The projection kills the classes of scalar matrices.

@[simp]

theorem TauCeti.relativeAlgebraicK1.coe_projection_mul_map_algebraMap {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] (x : AlgebraicK1 (Unitization R A)) : ↑((projection R A) x) * (AlgebraicK1.map ((algebraMap R (Unitization R A)).comp ↑(Unitization.fstHom R A))) x = x

Every class of A⁺ is the product of its relative part and the class of a scalar matrix, the image of x under the map induced by s ∘ ε.

noncomputable def TauCeti.relativeAlgebraicK1.map {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} [NonUnitalRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) : ↥(relativeAlgebraicK1 R A) →* ↥(relativeAlgebraicK1 R B)

The homomorphism of relative K₁ induced by a homomorphism of nonunital algebras, through the induced map of forced unitizations.

@[simp]

theorem TauCeti.relativeAlgebraicK1.coe_map_apply {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} [NonUnitalRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) (x : ↥(relativeAlgebraicK1 R A)) : ↑((map f) x) = (AlgebraicK1.map ↑(Unitization.map f)) ↑x

The induced homomorphism of relative K₁ is the induced homomorphism of K₁(A⁺).

theorem TauCeti.relativeAlgebraicK1.map_projection {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} [NonUnitalRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] (f : A →ₙₐ[R] B) (x : AlgebraicK1 (Unitization R A)) : (map f) ((projection R A) x) = (projection R B) ((AlgebraicK1.map ↑(Unitization.map f)) x)

The projection onto relative K₁ is natural for homomorphisms of nonunital algebras.

@[simp]

theorem TauCeti.relativeAlgebraicK1.map_id {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] : map (NonUnitalAlgHom.id R A) = MonoidHom.id ↥(relativeAlgebraicK1 R A)

The identity homomorphism induces the identity of relative K₁.

theorem TauCeti.relativeAlgebraicK1.map_comp {R : Type u_1} {A : Type u_2} [CommRing R] [NonUnitalRing A] [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] {B : Type u_3} {C : Type u_4} [NonUnitalRing B] [Module R B] [IsScalarTower R B B] [SMulCommClass R B B] [NonUnitalRing C] [Module R C] [IsScalarTower R C C] [SMulCommClass R C C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C) : map (g.comp f) = (map g).comp (map f)

Relative K₁ is functorial.