Skip to content

Instantly share code, notes, and snippets.

@kckennylau

kckennylau/free_group.lean Secret

Created Apr 17, 2018
Embed
What would you like to do?
import data.list.basic data.quot algebra.group
universes u v
variables (α : Type u)
namespace free_group
inductive rel : list (α × bool) → list (α × bool) → Prop
| refl {L} : rel L L
| symm {L₁ L₂} : rel L₁ L₂ → rel L₂ L₁
| trans {L₁ L₂ L₃} : rel L₁ L₂ → rel L₂ L₃ → rel L₁ L₃
| append {L₁ L₂ L₃ L₄} : rel L₁ L₃ → rel L₂ L₄ → rel (L₁ ++ L₂) (L₃ ++ L₄)
| bnot {x b} : rel [(x, b), (x, bnot b)] []
instance setoid : setoid (list (α × bool)) :=
⟨rel α,
λ L, rel.refl α,
λ L₁ L₂, rel.symm,
λ L₁ L₂ L₃, rel.trans⟩
end free_group
def free_group : Type u :=
quotient (free_group.setoid α)
namespace free_group
lemma reverse_map_bnot {L₁ L₂} (H : rel α L₁ L₂) :
rel α (L₁.map $ λ (x : α × bool), (x.1, bnot x.2)).reverse
(L₂.map $ λ (x : α × bool), (x.1, bnot x.2)).reverse :=
begin
induction H with L1 L1 L2 H1 ih1 L1 L2 L3 H1 H2 ih1 ih2
L1 L2 L3 L4 H1 H2 ih1 ih2 x b,
case rel.refl
{ apply rel.refl },
case rel.symm
{ apply rel.symm, assumption },
case rel.trans
{ apply rel.trans, assumption, assumption },
case rel.append
{ rw [list.map_append, list.map_append],
rw [list.reverse_append, list.reverse_append],
apply rel.append,
assumption, assumption },
case rel.bnot
{ dsimp [list.reverse, list.reverse_core],
rw [bnot_bnot],
apply rel.bnot }
end
lemma reverse_map_bnot_append {L : list (α × bool)} :
(L.map $ λ (x : α × bool), (x.1, bnot x.2)).reverse ++ L ≈ list.nil :=
begin
induction L with h t ih,
case list.nil
{ refl },
case list.cons
{ apply rel.trans _ ih,
rw [list.map_cons, list.reverse_cons', list.append_assoc],
apply rel.append,
{ apply rel.refl },
{ change rel α ([(h.fst, bnot (h.snd))] ++ [h] ++ t) ([] ++ t),
apply rel.append,
{ cases h with x b,
have H := @rel.bnot α x (bnot b),
rwa bnot_bnot at H },
{ apply rel.refl } } }
end
instance group : group (free_group α) :=
{ mul := @quotient.lift₂ _ _ _ (free_group.setoid α) _ (λ L₁ L₂, ⟦L₁ ++ L₂⟧) $
λ L₁ L₂ L₃ L₄ H13 H24, quotient.sound $ rel.append H13 H24,
one := ⟦[]⟧,
inv := @quotient.lift _ _ (free_group.setoid α) (λ L, ⟦(L.map $ λ (x : α × bool), (x.1, bnot x.2)).reverse⟧) $
λ L₁ L₂ H, quotient.sound $ reverse_map_bnot α H,
mul_assoc := λ x y z, quotient.induction_on₃ x y z $ λ m n p, quotient.sound $ by rw [list.append_assoc],
one_mul := λ x, quotient.induction_on x $ λ L, quotient.sound $ by refl,
mul_one := λ x, quotient.induction_on x $ λ L, quotient.sound $ by rw list.append_nil,
mul_left_inv := λ x, quotient.induction_on x $ λ L, quotient.sound $
reverse_map_bnot_append α }
def of_type : α → free_group α :=
λ x, ⟦[(x, tt)]⟧
section to_group
variables {α} {β : Type v} [group β] (f : α → β)
def to_group.aux : α × bool → β :=
λ x, bool.rec_on x.2 (f x.1)⁻¹ (f x.1)
def to_group : free_group α → β :=
λ x, quotient.lift_on x (λ L : list _, list.prod $ L.map $ to_group.aux f) $
begin
intros L₁ L₂ H,
induction H with L1 L1 L2 H1 ih1 L1 L2 L3 H1 H2 ih1 ih2
L1 L2 L3 L4 H1 H2 ih1 ih2 x b,
case rel.refl
{ refl },
case rel.symm
{ symmetry, assumption },
case rel.trans
{ transitivity, assumption, assumption },
case rel.append
{ dsimp at ih1 ih2 ⊢,
rw [list.map_append, list.map_append],
rw [list.prod_append, list.prod_append],
rw [ih1, ih2] },
case rel.bnot
{ cases b;
simp [to_group.aux, list.prod] }
end
instance to_group.is_group_hom : is_group_hom (to_group f) :=
λ x y, quotient.induction_on₂ x y $ λ L₁ L₂,
show to_group f (⟦L₁ ++ L₂⟧) = to_group f ⟦L₁⟧ * to_group f ⟦L₂⟧,
by simp [to_group]
theorem to_group.of_type (x) : to_group f (of_type α x) = f x :=
one_mul _
end to_group
end free_group
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment