Homotopy Type Theory
abelian group homomorphism > history (Rev #4, changes)
Showing changes from revision #3 to #4:
Added | Removed | Changed
Definition
< abelian group homomorphism
For abelian group s ( A , 0 A , + A , − A ) (A, 0_A, +_A, -_A) and ( B , 0 B , + B , − B ) (B, 0_B, +_B, -_B) and a function f : A → B f:A \to B , let us define the types
preservesUnit ( f ) ≔ f ( 0 A ) = B 0 b preservesUnit(f) \coloneqq f(0_A) =_B 0_b preservesAddition ( f ) ≔ ∏ a : A ∏ b : A f ( a + A b ) = B f ( a ) + B f ( b ) preservesAddition(f) \coloneqq \prod_{a:A} \prod_{b:A} f(a +_A b) =_B f(a) +_B f(b) preservesNegation ( f ) ≔ ∏ a : A f ( − A ( a ) ) = B − B ( f ( a ) ) preservesNegation(f) \coloneqq \prod_{a:A} f(-_A(a)) =_B -_B(f(a)) isAbGrpHom ( f ) ≔ preservesUnit ( f ) × preservesAddition ( f ) × preservesNegation ( f ) isAbGrpHom(f) \coloneqq preservesUnit(f) \times preservesAddition(f) \times preservesNegation(f)
f f abelian group homomorphism if isAbGrpHom ( f ) isAbGrpHom(f) set , the identity types are proposition s and thus preserved in an abelian group homomorphism.
The type of abelian group homomorphisms between abelian groups A A B B
Hom Ab ( A , B ) ≔ ∏ f : A → B isAbGrpHom ( f ) Hom_{Ab}(A, B) \coloneqq \prod_{f:A\to B} isAbGrpHom(f)
See also
Revision on June 17, 2022 at 20:38:06 by
Anonymous? .
See the history of this page for a list of all contributions to it.