michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Add product_inl and product_inr.

Browse source
This commit is contained in:
favonia 2017-06-07 09:41:41 -06:00
parent 607e5343b1
commit f84cebe13c
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
algebra/product_group.hlean
View file

@ -61,6 +61,12 @@ namespace group
infix ` ×g `:60 := group.product
infix ` ×ag `:60 := group.ab_product
definition product_inl (G H : Group) : G →g G ×g H :=
homomorphism.mk (λx, (x, one)) (λx y, prod_eq !refl !one_mul⁻¹)
definition product_inr (G H : Group) : H →g G ×g H :=
homomorphism.mk (λx, (one, x)) (λx y, prod_eq !one_mul⁻¹ !refl)
definition product_functor [constructor] {G G' H H' : Group} (φ : G →g H) (ψ : G' →g H') :
G ×g G' →g H ×g H' :=
homomorphism.mk (λx, (φ x.1, ψ x.2)) (λx y, prod_eq !to_respect_mul !to_respect_mul)