Homotopy Type Theory
function algebra > history (changes)
Showing changes from revision #2 to #3:
Added | Removed | Changed
Definition
< function algebra
Given a commutative ring R R and any type T T , the type of functions T → R T \to R has the structure of an R R -algebra, with canonical ring homomorphism c : R → ( T → R ) c:R \to (T \to R) being the constant functions in T → R T \to R . One could define the R R -algebra operations pointwise on R R :
r : R ⊢ 0 ( r ) ≔ 0 r:R \vdash 0(r) \coloneqq 0 r : R ⊢ ( f + g ) ( r ) ≔ f ( r ) + g ( r ) r:R \vdash (f + g)(r) \coloneqq f(r) + g(r) r : R ⊢ ( − f ) ( r ) ≔ − f ( r ) r:R \vdash (-f)(r) \coloneqq -f(r) r : R ⊢ 1 ( r ) ≔ 1 r:R \vdash 1(r) \coloneqq 1 r : R , s : R ⊢ ( s f ) ( r ) ≔ c ( s ) ⋅ f ( r ) r:R, s:R \vdash (s f)(r) \coloneqq c(s) \cdot f(r) r : R ⊢ ( f ⋅ g ) ( r ) ≔ f ( r ) ⋅ g ( r ) r:R \vdash (f \cdot g)(r) \coloneqq f(r) \cdot g(r)
There is also the identity function on R R
See also
Last revised on June 15, 2022 at 01:44:36.
See the history of this page for a list of all contributions to it.