infinite elementary linear group functor

Definition

the infinite elementary linear group functor is defined as functor

20241017-infinite_elementary_linear_group_functor_fc5c14f3c20b1802c339b56dbcbf6c18ba7f52e8.svg

see:

Proof

follows from:

where the inclusion 20241017-infinite_elementary_linear_group_functor_37fb7260775d55e19d89783ba47ea277958f970b.svg is a natural transformation, hence

20241017-infinite_elementary_linear_group_functor_15e5d3c02c17dfcc5fe35b73bf2c3d28eddd88f3.svg

commutes

Date: nil

Author: Anton Zakrewski

Created: 2025-01-15 Mi 17:25