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

unbundle set in direct_sum

Browse source
This commit is contained in:
Floris van Doorn 2017-06-07 11:30:09 -04:00
parent 5fdc8ad2c8
commit 984d564cc6
3 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
algebra/direct_sum.hlean
View file

@ -14,10 +14,10 @@ namespace group
section
parameters {I : Set} (Y : I → AbGroup)
parameters {I : Type} [is_set I] (Y : I → AbGroup)
variables {A' : AbGroup} {Y' : I → AbGroup}
definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
definition dirsum_carrier : AbGroup := free_ab_group (Σi, Y i)
local abbreviation ι [constructor] := @free_ab_group_inclusion
inductive dirsum_rel : dirsum_carrier → Type :=
| rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹)

2
algebra/free_commutative_group.hlean
View file

@ -15,7 +15,7 @@ namespace group
variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
variables (X : Set) {Y : Set} {l l' : list (X ⊎ X)}
variables (X : Type) {Y : Type} [is_set X] [is_set Y] {l l' : list (X ⊎ X)}
/- Free Abelian Group of a set -/
namespace free_ab_group

8
algebra/free_group.hlean
View file

@ -15,7 +15,7 @@ namespace group
variables {G G' : Group} {g g' h h' k : G} {A B : AbGroup}
/- Free Group of a set -/
variables (X : Set) {l l' : list (X ⊎ X)}
variables (X : Type) [is_set X] {l l' : list (X ⊎ X)}
namespace free_group
inductive free_group_rel : list (X ⊎ X) → list (X ⊎ X) → Type :=
@ -60,10 +60,10 @@ namespace group
end
definition free_group_one [constructor] : FG X := class_of []
definition free_group_inv [unfold 3] : FG X → FG X :=
definition free_group_inv [unfold 4] : FG X → FG X :=
quotient_unary_map (reverse ∘ map sum.flip)
(λl l', trunc_functor -1 (rel_respect_reverse ∘ rel_respect_flip))
definition free_group_mul [unfold 3 4] : FG X → FG X → FG X :=
definition free_group_mul [unfold 4 5] : FG X → FG X → FG X :=
quotient_binary_map append (λl l', trunc.elim (λr m m', trunc.elim (λs, tr (resp_append r s))))
section
@ -123,7 +123,7 @@ namespace group
definition free_group_inclusion [constructor] (x : X) : free_group X :=
class_of [inl x]
definition fgh_helper [unfold 5] (f : X → G) (g : G) (x : X + X) : G :=
definition fgh_helper [unfold 6] (f : X → G) (g : G) (x : X + X) : G :=
g * sum.rec (λx, f x) (λx, (f x)⁻¹) x
theorem fgh_helper_respect_rel (f : X → G) (r : free_group_rel X l l')