Continuous affine maps. #
This file defines a type of bundled continuous affine maps.
Note that the definition and basic properties established here require minimal assumptions, and do not even assume compatibility between the topological and algebraic structures. Of course it is necessary to assume some compatibility in order to obtain a useful theory. Such a theory is developed elsewhere for affine spaces modelled on normed vector spaces, but not yet for general topological affine spaces (since we have not defined these yet).
Main definitions: #
- toFun : P → Q
- cont : Continuous s.toFun
A continuous map of affine spaces.
Helper instance for when there's too many metavariables to apply
Forgetting its algebraic properties, a continuous affine map is a continuous map.
The constant map is a continuous affine map.
The composition of morphisms is a morphism.
A continuous linear map can be regarded as a continuous affine map.