Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Making a group from first principles, live streamed on Twitch 25/6/20, with Lean 3.16.4
import tactic
/-
Making group theory in a theorem prover
-/
namespace mygroup
-- A group needs multiplication, inverse, identity
class group (G : Type) extends has_mul G, has_inv G, has_one G :=
-- axioms go here
(mul_assoc : ∀ (a b c : G), (a * b) * c = a * (b * c))
(one_mul : ∀ (a : G), 1 * a = a)
(mul_left_inv : ∀ (a : G), a⁻¹ * a = 1)
/-
non-example of a group: G is any non-empty set, 1 is any element,
and define g * h = h, g⁻¹ = 1 for all g
NOT A GROUP because mul_left_inv fails
-/
namespace group
attribute [simp] mul_left_inv one_mul
variables {G : Type} [group G]
-- Students at my uni also learn that mul_one : a * 1 = a and mul_right_inv are axioms
-- let's prove them!
-- let's start by showing you can cancel on the left
lemma mul_left_cancel (a b c : G) (H : a * b = a * c) : b = c :=
calc b = 1 * b : by rw one_mul
... = (a⁻¹ * a) * b : by rw mul_left_inv
... = a⁻¹ * (a * b) : by rw mul_assoc
... = a⁻¹ * (a * c) : by rw H
... = (a⁻¹ * a) * c : by rw mul_assoc
... = 1 * c : by rw mul_left_inv
... = c : by rw one_mul
-- that proof is nice to look at
lemma mul_left_cancel' (a b c : G) (H : a * b = a * c) : b = c :=
by rw [←one_mul b, ←mul_left_inv a, mul_assoc, H, ←mul_assoc, mul_left_inv, one_mul]
lemma mul_eq_of_eq_inv_mul {a x y : G} (h : x = a⁻¹ * y) : a * x = y :=
begin
apply mul_left_cancel a⁻¹,
rw ←mul_assoc,
-- ⊢ (a⁻¹ * a) * x = a⁻¹ * y
-- know : x = a⁻¹ * y
-- simplifier can now do the rest
simp [h],
end
@[simp] lemma mul_one (a : G) : a * 1 = a :=
begin
apply mul_eq_of_eq_inv_mul,
simp,
end
-- term mode proof
lemma mul_one' (a : G) : a * 1 = a :=
mul_eq_of_eq_inv_mul $ by simp
@[simp] lemma mul_right_inv (a : G) : a * a⁻¹ = 1 :=
begin
apply mul_eq_of_eq_inv_mul,
simp,
end
@[simp] lemma inv_mul_right_cancel (a b : G) : (b * a⁻¹) * a = b := by simp [mul_assoc]
@[simp] lemma mul_inv_right_cancel (a b : G) : (b * a) * a⁻¹ = b := by simp [mul_assoc]
@[simp] lemma inv_mul_left_cancel (a b : G) : a⁻¹ * (a * b) = b := by simp [←mul_assoc]
example (a b c : G) : a * a⁻¹ * a⁻¹ * a = 1 := by simp
example (a b c : G) : a * a⁻¹ * b * a * a⁻¹ = b := by simp
example (a b c : G) : a * a⁻¹ * b * c * c⁻¹ * b⁻¹ = 1 := by simp
example (a b c : G) : b * c * c⁻¹ * b⁻¹ * a * a⁻¹ = 1 := by simp
@[simp] lemma mul_eq_iff_eq_inv_mul {a x y : G} : x = a⁻¹ * y ↔ a * x = y :=
begin
split,
{ apply mul_eq_of_eq_inv_mul},
{ intro h,
simp [h.symm]}
end
@[simp] lemma mul_eq_iff_eq_inv_mul' {a x y : G} : a⁻¹ * y = x ↔ y = a * x :=
by simp [eq_comm]
@[simp] lemma mul_left_cancel_iff (a b c : G) : a * b = a * c ↔ b = c :=
begin
split,
{ apply mul_left_cancel},
{ rintro rfl, refl}
end
example (a b c : G) : a * b * c * (c⁻¹ * a * a⁻¹) = a * c * c⁻¹ * b := by simp
-- this is exactly what the simplifier is good at
end group
structure subgroup (G : Type) [group G] :=
-- carrier is the name of the subset
(carrier : set G)
(one_mem' : (1 : G) ∈ carrier)
(inv_mem' {x} : x ∈ carrier → x⁻¹ ∈ carrier)
(mul_mem' {x y} : x ∈ carrier → y ∈ carrier → x * y ∈ carrier)
namespace subgroup
variables {G : Type} [group G] (H J K : subgroup G) (a b c : G)
-- want to be able to say a ∈ H
instance : has_mem G (subgroup G) := ⟨λ g H, g ∈ H.carrier⟩
-- want to talk about H₁ ≤ H₂ (meanning H₁ ⊆ H₂)
-- "subgroups of a group form a lattice"
instance : has_le (subgroup G) := ⟨λ S T, S.carrier ⊆ T.carrier⟩
lemma le_def (H J : subgroup G) : H.carrier ≤ J.carrier ↔ H ≤ J := iff.rfl
@[ext] theorem ext {H J : subgroup G} (h : ∀ (x : G), x ∈ H ↔ x ∈ J) : H = J :=
begin
cases H,
cases J,
suffices : H_carrier = J_carrier,
simpa,
ext x,
exact h x,
end
lemma mem_coe {g : G} : g ∈ H.carrier ↔ g ∈ H := iff.rfl
theorem one_mem : (1 : G) ∈ H := H.one_mem'
theorem mul_mem {x y : G} : x ∈ H → y ∈ H → x * y ∈ H := subgroup.mul_mem' H
theorem inv_mem {x : G} : x ∈ H → x⁻¹ ∈ H := subgroup.inv_mem' H
-- definition in Lean because `subgroup` contains data
/-- "Theorem" : intersection of two subgroups is a subgroup -/
def inf (H K : subgroup G) : subgroup G :=
{ carrier := H.carrier ∩ K.carrier,
one_mem' := ⟨H.one_mem', K.one_mem'⟩,
inv_mem' := λ x ⟨hH, hK⟩, ⟨H.inv_mem' hH, K.inv_mem' hK⟩,
mul_mem' := λ x y ⟨hxH, hxK⟩ ⟨hyH, hyK⟩, ⟨H.mul_mem' hxH hyH, K.mul_mem' hxK hyK⟩ }
open set
-- intersection of any number of subgroups is a subgroup
def Infi (ι : Type) (H : ι → subgroup G) : subgroup G :=
{ carrier := ⋂(i : ι), (H i).carrier,
one_mem' := begin
rw mem_Inter,
intro i,
apply subgroup.one_mem',
end,
inv_mem' := begin
intro x,
intro hx,
rw mem_Inter at hx ⊢,
intro i,
apply subgroup.inv_mem',
tauto!,
end,
mul_mem' := begin
intros x y hx hy,
rw mem_Inter at *,
intro i,
apply subgroup.mul_mem';
tauto!,
end }
-- why is H bug not fixed?
def Inf (S : set (subgroup G)) : subgroup G :=
{ carrier := -- ⋂₀ {H.carrier | H ∈ S},
-- ⋂₀ {T : set G | ∃ J ∈ S, T = subgroup.carrier J},
Inf (subgroup.carrier '' S),
one_mem' := begin
rw mem_sInter,
rintro t ⟨⟨H_w_carrier, H_w_one_mem', H_w_inv_mem', H_w_mul_mem'⟩, H_h_w, rfl⟩,
apply subgroup.one_mem',
end,
inv_mem' := begin
intros x hx,
rw mem_sInter at hx ⊢,
rintro t ⟨H, H_h_w, rfl⟩,
apply H.inv_mem',
apply hx,
use H,
tauto!,
end,
mul_mem' := begin
intros x y hx hy,
rw mem_sInter at hx hy ⊢,
rintro t ⟨H, hH, rfl⟩,
apply H.mul_mem',
apply hx, use H, tauto,
apply hy, use H, tauto,
end }
instance : has_Inf (subgroup G) := ⟨Inf⟩
#check complete_lattice_of_Inf
-- goal -- make subgroups of a group into a complete lattice
/-
complete_lattice_of_Inf :
Π (α : Type u_1) [H1 : partial_order α] [H2 : has_Inf α],
(∀ (s : set α), is_glb s (Inf s)) → complete_lattice α
-/
instance : partial_order (subgroup G) :=
{ le := (≤),
le_refl := by tidy,
le_trans := by tidy,
le_antisymm := by tidy }
instance : complete_lattice (subgroup G) := complete_lattice_of_Inf _ begin
intro S,
apply @is_glb.of_image _ _ _ _ subgroup.carrier,
intros, refl,
apply is_glb_Inf,
end
-- adjoint functor to carrier functor is the span functor
-- from subsets to subgroups
def span (S : set G) : subgroup G := Inf {H : subgroup G | S ⊆ H.carrier}
lemma monotone_carrier : monotone (subgroup.carrier : subgroup G → set G) :=
λ H J, id
lemma monotone_span : monotone (span : set G → subgroup G) :=
λ S T h, Inf_le_Inf $ λ H hH x hx, hH $ h hx
lemma subset_span (S : set G) : S ≤ (span S).carrier :=
begin
rintro x hx _ ⟨H, hH, rfl⟩,
exact hH hx,
end
lemma span_subgroup (H : subgroup G) : span H.carrier = H :=
begin
ext,
split,
{ intro hx,
unfold span at hx,
replace hx := mem_sInter.1 hx,
apply hx,
use H,
simp,
tauto! },
{ intro h,
apply subset_span,
exact h},
end
-- the functors are adjoint
def gi_subgroup : galois_insertion span (@subgroup.carrier G _) :=
galois_insertion.monotone_intro monotone_carrier monotone_span subset_span span_subgroup
-- claim : if g ∈ G then the map ℤ → G, n ↦ g^n is a group hom. Duh.
/-- definition of map sending g, n to gⁿ , n ∈ ℕ -/
def pow (g : G) : ℕ → G
| 0 := 1
| (n+1) := pow n * g -- $6,000,000 : do I do that or g * pow n ??
#check nat.iterate
--example {α : Type} (h : α ≃ α) : ℤ → α ≃ α := by hint
#print notation -[
#print function.combine
#check function.bicompl
#check fish -- wtf?
def pow' (g : G) (n : ℕ) := ((*) g)^[n] 1
open int
def int.iterate {α : Type} (h : α ≃ α) : ℤ → α → α
| (of_nat n) := h^[n]
| (neg_succ_of_nat n) := h.symm^[n+1]
notation f`^⦃`:91 n`⦄`:91 := int.iterate f n
namespace int.iterate
variables {α : Type} (h : α ≃ α)
example (a b : ℕ) : h^[a+b] = (h^[a]) ∘ (h^[b]) := sorry -- brackets needed
@[simp] lemma zero : h^⦃0⦄ = id := rfl
@[simp] lemma one : h^⦃1⦄ = h := by funext; refl --rfl --funext $ λ x, rfl
@[simp] lemma neg_one : h^⦃-1⦄ = h.symm := funext $ λ x, rfl -- :-)
lemma neg (a : ℤ) : h^⦃-a⦄ = h.symm^⦃a⦄ :=
begin
cases a,
cases a,
ext, refl,
ext, refl,
ext, refl,
end
example (i : ℕ) : -[1+ i] = -((i : ℤ) + 1) := by exact neg_succ_of_nat_eq i
lemma add_one (a : ℤ) : h^⦃a+1⦄ = h^⦃a⦄ ∘ h :=
begin
cases a with i i,
{ refl},
{ suffices : h^⦃(-↑i)⦄ = h^⦃-(i + 1)⦄ ∘ h,
convert this, rw neg_succ_of_nat_eq, ring,
rw neg,
rw neg,
ext,
norm_cast,
have : h.symm^⦃↑i⦄ ∘ h.symm = h.symm^⦃↑(i + 1)⦄,
refl,
rw ←this,
simp},
end
lemma sub_one (a : ℤ) : h^⦃a-1⦄ = h^⦃a⦄ ∘ h.symm :=
begin
rw ←neg_one,
rw ←h.symm_symm,
rw ←neg,
rw (show -(a-1)=-a+1, by ring),
rw add_one,
simp [neg],
end
lemma add (a b : ℤ) : h^⦃a + b⦄ = h^⦃a⦄ ∘ h^⦃b⦄ :=
begin
apply int.induction_on b,
{simp},
{ intro i,
intro useful,
rw ←add_assoc,
rw add_one,
rw useful,
rw add_one,
},
{ intro i,
intro useful,
rw ←add_sub_assoc,
rw sub_one,
rw useful,
rw sub_one,
},
end
end int.iterate
-- def pow_hom (g : G) (a b : ℕ) : pow g a * pow g b = pow g (a + b) :=
-- begin
-- sorry
-- end
-- /-- definition of map sending g, n to gⁿ , n ∈ ℤ -/
-- def zpow (g : G) : ℤ → G
-- | (of_nat n) := pow g n
-- | (neg_succ_of_nat n) := pow g⁻¹ (n+1)
--example (g : G) : G ≃ G := by suggest
def thing (g : G) : G ≃ G :=
{ to_fun := (* g),
inv_fun := (* g⁻¹),
left_inv := by intro x; simp,
right_inv := by intro x; simp }
open int.iterate
lemma foo (g j : G) (a : ℤ) : j * (thing g^⦃a⦄ 1) = thing g^⦃a⦄ j :=
begin
revert j,
apply int.induction_on a,
{ simp},
{ intro i,
intro hi,
intro j,
rw int.iterate.add_one,
unfold function.comp,
rw ←hi (thing _ j),
rw ←hi,
unfold thing, simp [mygroup.group.mul_assoc],
},
{ intro i,
intro hi,
intro j,
rw int.iterate.sub_one,
unfold function.comp,
conv_rhs begin
rw ←hi,
end,
rw ←hi,
unfold thing, simp [mygroup.group.mul_assoc],
}
end
def zpow' (g : G) : ℤ → G := λ z, (thing g)^⦃z⦄ 1
instance : has_pow G ℤ := ⟨zpow'⟩
lemma zpow_hom (g : G) (a b : ℤ) : g^a * g^b = g^(a + b) :=
begin
unfold has_pow.pow,
unfold zpow',
rw add_comm,
rw int.iterate.add,
unfold function.comp,
rw foo,
end
/-- The subgroup generated by an element of a group equals the set of integer number powers of
the element. -/
lemma mem_span_singleton {x y : G} : y ∈ span ({x} : set G) ↔ ∃ n : ℤ, x ^ n = y :=
begin
sorry
end
end subgroup
end mygroup
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment