infinite general linear group functor

Definition

the infinite general linear group functor is defined as functor

20241017-infinite_general_linear_group_functor_193faf7912fa584ad06308ef8eb09577a8547224.svg

see:

Proof

follows from:

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

20241017-infinite_general_linear_group_functor_9213aebcf5f40c6714172872eece7a0cb12d9975.svg

commutes

Date: nil

Author: Anton Zakrewski

Created: 2025-01-15 Mi 17:46