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

add some constructor attributes to product_group

Browse source
This commit is contained in:
Floris van Doorn 2017-06-08 11:41:37 -04:00
parent 4ca9907929
commit 664d971d4b
2 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
algebra/direct_sum.hlean
View file

@ -93,7 +93,7 @@ namespace group
let branch := bool.rec G H in
let to_hom := (dirsum_elim (bool.rec (product_inl G H) (product_inr G H))
: dirsum (bool.rec G H) →g G ×ag H) in
let from_hom := (Group_sum_elim G H (dirsum (bool.rec G H))
let from_hom := (Group_sum_elim (dirsum (bool.rec G H))
(dirsum_incl branch bool.ff) (dirsum_incl branch bool.tt)
: G ×g H →g dirsum branch) in
begin

10
algebra/product_group.hlean
View file

@ -61,18 +61,18 @@ namespace group
infix ` ×g `:60 := group.product
infix ` ×ag `:60 := group.ab_product
definition product_inl (G H : Group) : G →g G ×g H :=
definition product_inl [constructor] (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 :=
definition product_inr [constructor] (G H : Group) : H →g G ×g H :=
homomorphism.mk (λx, (one, x)) (λx y, prod_eq !one_mul⁻¹ !refl)
definition Group_sum_elim (G H : Group) (I : AbGroup) (φ : G →g I) (ψ : H →g I) : G ×g H →g I :=
homomorphism.mk (λx, φ x.1 * ψ x.2) (λx y, calc
definition Group_sum_elim [constructor] {G H : Group} (I : AbGroup) (φ : G →g I) (ψ : H →g I) : G ×g H →g I :=
homomorphism.mk (λx, φ x.1 * ψ x.2) abstract (λx y, calc
φ (x.1 * y.1) * ψ (x.2 * y.2) = (φ x.1 * φ y.1) * (ψ x.2 * ψ y.2)
: by exact ap011 mul (to_respect_mul φ x.1 y.1) (to_respect_mul ψ x.2 y.2)
... = (φ x.1 * ψ x.2) * (φ y.1 * ψ y.2)
: by exact interchange I (φ x.1) (φ y.1) (ψ x.2) (ψ y.2))
: by exact interchange I (φ x.1) (φ y.1) (ψ x.2) (ψ y.2)) end
definition product_functor [constructor] {G G' H H' : Group} (φ : G →g H) (ψ : G' →g H') :
G ×g G' →g H ×g H' :=