Homotopy Type Theory algebra (ring theory) > history (Rev #3, changes)

Showing changes from revision #2 to #3: Added | Removed | Changed

Definition

Given a ring RR, an RR-algebra is a ring AA with a ring homomorphism? f:RAf:R \to A.

Properties

If RR is a commutative ring and the RR-algebra AA has a commutative ring homomorphism? g:RZ(A)g:R \to Z(A) into the center Z(A)AZ(A) \subseteq A of AA, as well as a term a:ig=fa: i \circ g = f, where i:Z(A)Ai:Z(A) \subseteq A is the associated monic function for subtype Z(A)Z(A) of AA, then AA is an associative? unital? algebra in module theory.

See also

Revision on June 13, 2022 at 20:09:16 by Anonymous?. See the history of this page for a list of all contributions to it.