forked from leanprover/lean2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtrunc_group.hlean
113 lines (86 loc) · 2.85 KB
/
trunc_group.hlean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
/-
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Floris van Doorn
truncating an ∞-group to a group
-/
import hit.trunc algebra.bundled
open eq is_trunc trunc
namespace algebra
section
parameters (n : trunc_index) {A : Type} [inf_group A]
local abbreviation G := trunc n A
definition trunc_mul [unfold 9 10] (g h : G) : G :=
begin
induction g with p,
induction h with q,
exact tr (p * q)
end
definition trunc_inv [unfold 9] (g : G) : G :=
begin
induction g with p,
exact tr p⁻¹
end
definition trunc_one [constructor] : G :=
tr 1
local notation 1 := trunc_one
local postfix ⁻¹ := trunc_inv
local infix * := trunc_mul
theorem trunc_mul_assoc (g₁ g₂ g₃ : G) : g₁ * g₂ * g₃ = g₁ * (g₂ * g₃) :=
begin
induction g₁ with p₁,
induction g₂ with p₂,
induction g₃ with p₃,
exact ap tr !mul.assoc,
end
theorem trunc_one_mul (g : G) : 1 * g = g :=
begin
induction g with p,
exact ap tr !one_mul
end
theorem trunc_mul_one (g : G) : g * 1 = g :=
begin
induction g with p,
exact ap tr !mul_one
end
theorem trunc_mul_left_inv (g : G) : g⁻¹ * g = 1 :=
begin
induction g with p,
exact ap tr !mul.left_inv
end
parameter (A)
definition inf_group_trunc [constructor] [instance] : inf_group (trunc n A) :=
⦃inf_group,
mul := algebra.trunc_mul n,
mul_assoc := algebra.trunc_mul_assoc n,
one := algebra.trunc_one n,
one_mul := algebra.trunc_one_mul n,
mul_one := algebra.trunc_mul_one n,
inv := algebra.trunc_inv n,
mul_left_inv := algebra.trunc_mul_left_inv n⦄
definition group_trunc [constructor] : group (trunc 0 A) :=
group_of_inf_group _
end
definition igtrunc [constructor] (n : ℕ₋₂) (A : InfGroup) : InfGroup :=
InfGroup.mk (trunc n A) (inf_group_trunc n A)
definition gtrunc [constructor] (A : InfGroup) : Group :=
Group.mk (trunc 0 A) (group_trunc A)
section
variables (n : trunc_index) {A : Type} [ab_inf_group A]
theorem trunc_mul_comm (g h : trunc n A) : trunc_mul n g h = trunc_mul n h g :=
begin
induction g with p,
induction h with q,
exact ap tr !mul.comm
end
variable (A)
definition ab_inf_group_trunc [constructor] [instance] : ab_inf_group (trunc n A) :=
⦃ab_inf_group, inf_group_trunc n A, mul_comm := algebra.trunc_mul_comm n⦄
definition ab_group_trunc [constructor] : ab_group (trunc 0 A) :=
ab_group_of_ab_inf_group _
definition aigtrunc [constructor] (n : ℕ₋₂) (A : AbInfGroup) : AbInfGroup :=
AbInfGroup.mk (trunc n A) (ab_inf_group_trunc n A)
definition agtrunc [constructor] (A : AbInfGroup) : AbGroup :=
AbGroup.mk (trunc 0 A) (ab_group_trunc A)
end
end algebra