monoid_universal_enveloping_group.lean

import algebra

/-!
# Universal enveloping group of a monoid

`envel_gp M` is the universal group that factors homomorphisms from a
given monoid to a group.

For a monoid action on a type `α`, `envel_action M α` is the universal
action that factors homomorphisms of a given monoid action to a group
action.

`quoA M α` is the quotient of `α` by the monoid action `M` using `quot`.

`quoB M α` is the quotient of `envel_action M α` by the group `envel_gp M`.

`quoA_equiv_quoB` is the equivalence between these two.

(Reference for the enveloping group: Bergman, "An invitation to
general algebra and universal constructions.")

-/

universes u v

/--
Formal expressions for group generated by M.
-/
inductive pre_envel_gp (M : Type*)
| incl (x : M) : pre_envel_gp
| mul (a b : pre_envel_gp) : pre_envel_gp
| inv (a : pre_envel_gp) : pre_envel_gp

open pre_envel_gp

/--
Relations on `pre_envel_gp M` for group with relations drawn from the monoid M.
-/
inductive pre_envel_gp_rel' (M : Type u) [monoid M] : pre_envel_gp M → pre_envel_gp M → Type u
| refl {a : pre_envel_gp M} : pre_envel_gp_rel' a a
| symm {a b : pre_envel_gp M} (h : pre_envel_gp_rel' a b) : pre_envel_gp_rel' b a
| trans {a b c : pre_envel_gp M} (hab : pre_envel_gp_rel' a b) (hbc : pre_envel_gp_rel' b c) : pre_envel_gp_rel' a c
| congr_mul (a b a' b' : pre_envel_gp M) (ha : pre_envel_gp_rel' a a') (hb : pre_envel_gp_rel' b b') : pre_envel_gp_rel' (mul a b) (mul a' b')
| congr_inv (a a' : pre_envel_gp M) (ha : pre_envel_gp_rel' a a') : pre_envel_gp_rel' (inv a) (inv a')
| assoc (a b c : pre_envel_gp M) : pre_envel_gp_rel' (mul (mul a b) c) (mul a (mul b c))
| one_mul (a : pre_envel_gp M) : pre_envel_gp_rel' (mul (incl 1) a) a
| mul_one (a : pre_envel_gp M) : pre_envel_gp_rel' (mul a (incl 1)) a
| mul_left_inv (a : pre_envel_gp M) : pre_envel_gp_rel' (mul (inv a) a) (incl 1)
| mul_incl (x y : M) : pre_envel_gp_rel' (mul (incl x) (incl y)) (incl (x * y))

/--
The above relation as a `Prop`.
-/
inductive pre_envel_gp_rel (M : Type u) [monoid M] : pre_envel_gp M → pre_envel_gp M → Prop
| rel {a b : pre_envel_gp M} (r : pre_envel_gp_rel' M a b) : pre_envel_gp_rel a b

def pre_envel_gp_rel'.rel {M : Type u} [monoid M] {a b : pre_envel_gp M} : pre_envel_gp_rel' M a b → pre_envel_gp_rel M a b :=
pre_envel_gp_rel.rel

@[refl]
lemma pre_envel_gp_rel.refl {M : Type u} [monoid M] {a : pre_envel_gp M} : pre_envel_gp_rel M a a :=
pre_envel_gp_rel.rel pre_envel_gp_rel'.refl

@[symm]
lemma pre_envel_gp_rel.symm {M : Type u} [monoid M] {a b : pre_envel_gp M} : pre_envel_gp_rel M a b → pre_envel_gp_rel M b a
| ⟨r⟩ := r.symm.rel

@[trans]
lemma pre_envel_gp_rel.trans {M : Type u} [monoid M] {a b c : pre_envel_gp M} :
  pre_envel_gp_rel M a b → pre_envel_gp_rel M b c → pre_envel_gp_rel M a c
| ⟨rab⟩ ⟨rbc⟩ := (rab.trans rbc).rel

instance pre_envel_gp.setoid (M : Type*) [monoid M] : setoid (pre_envel_gp M) :=
{ r := pre_envel_gp_rel M,
  iseqv := begin
    split, apply pre_envel_gp_rel.refl,
    split, apply pre_envel_gp_rel.symm,
    apply pre_envel_gp_rel.trans
  end }

/--
The universal enveloping group for the monoid M.
-/
def envel_gp (M : Type*) [monoid M] := quotient (pre_envel_gp.setoid M)

instance (M : Type*) [monoid M] : group (envel_gp M) :=
{ mul := λ a b, quotient.lift_on₂ a b
                  (λ a b, ⟦pre_envel_gp.mul a b⟧)
                  (λ a b a' b' ha hb,
                    begin cases ha, cases hb, apply quotient.sound, apply (pre_envel_gp_rel'.congr_mul a b a' b' ha_r hb_r).rel end),
  one := ⟦incl 1⟧,
  inv := λ a, quotient.lift_on a
                (λ a, ⟦pre_envel_gp.inv a⟧)
                (λ a a' ha,
                  begin cases ha, apply quotient.sound, apply (pre_envel_gp_rel'.congr_inv a a' ha_r).rel end),
  mul_assoc := λ a b c, begin
    refine quotient.ind (λ a, _) a,
    refine quotient.ind (λ b, _) b,
    refine quotient.ind (λ c, _) c,
    apply quotient.sound, exact (pre_envel_gp_rel'.assoc a b c).rel,
  end,
  one_mul := λ a, begin
    refine quotient.ind (λ a, _) a,
    apply quotient.sound, exact (pre_envel_gp_rel'.one_mul a).rel,
  end,
  mul_one := λ a, begin
    refine quotient.ind (λ a, _) a,
    apply quotient.sound, exact (pre_envel_gp_rel'.mul_one a).rel,
  end,
  mul_left_inv := λ a, begin
    refine quotient.ind (λ a, _) a,
    apply quotient.sound, exact (pre_envel_gp_rel'.mul_left_inv a).rel,
  end }

/--
The canonical homomorphism from a monoid to its enveloping group.
Satisfies universal properties defined by `to_envel_gp.map` and `to_envel_gp.univ`.
-/
def to_envel_gp (M : Type*) [monoid M] : M →* envel_gp M :=
{ to_fun := λ x, ⟦incl x⟧,
  map_one' := rfl,
  map_mul' := begin
    intros x y,
    apply quotient.sound, exact (pre_envel_gp_rel'.mul_incl x y).symm.rel,
  end }

def to_envel_gp.map_aux {M : Type*} [monoid M] {G : Type*} [group G] (f : M →* G) : pre_envel_gp M → G
| (incl x) := f x
| (mul a b) := to_envel_gp.map_aux a * to_envel_gp.map_aux b
| (inv a) := (to_envel_gp.map_aux a)⁻¹

namespace to_envel_gp.map_aux
open pre_envel_gp_rel'

lemma well_def {M : Type*} [monoid M] {G : Type*} [group G] (f : M →* G) :
  Π {a b : pre_envel_gp M}, pre_envel_gp_rel' M a b → to_envel_gp.map_aux f a = to_envel_gp.map_aux f b
| a b refl := rfl
| a b (symm h) := (well_def h).symm
| a b (trans hac hcb) := eq.trans (well_def hac) (well_def hcb)
| _ _ (congr_mul a b a' b' ha hb) := by { dsimp [to_envel_gp.map_aux], rw well_def ha, rw well_def hb, }
| _ _ (congr_inv a a' ha) := by { dsimp [to_envel_gp.map_aux], rw well_def ha }
| _ _ (assoc a b c) := by { apply mul_assoc }
| _ _ (one_mul a) := by { dsimp [to_envel_gp.map_aux], simp, }
| _ _ (mul_one a) := by { dsimp [to_envel_gp.map_aux], simp, }
| _ _ (mul_left_inv a) := by { dsimp [to_envel_gp.map_aux], simp, }
| _ _ (mul_incl x y) := by { dsimp [to_envel_gp.map_aux], simp, }

end to_envel_gp.map_aux

/--
Given a map from a monoid to a group, lift it to being a map from the enveloping group.
-/
def to_envel_gp.map {M : Type*} [monoid M] {G : Type*} [group G] (f : M →* G) : envel_gp M →* G :=
{ to_fun := λ x, quotient.lift_on x (to_envel_gp.map_aux f) begin
    intros a b hab, cases hab, apply to_envel_gp.map_aux.well_def f hab_r,
  end,
  map_one' := begin
    change quotient.lift_on ⟦incl 1⟧ (to_envel_gp.map_aux f) _ = 1,
    simp [to_envel_gp.map_aux],
  end,
  map_mul' := λ x y, begin
    refine quotient.ind (λ x, _) x,
    refine quotient.ind (λ y, _) y,
    change quotient.lift_on ⟦mul x y⟧ (to_envel_gp.map_aux f) _ = _,
    simp [to_envel_gp.map_aux],
  end }

/--
Given a homomorphism from a monoid to a group, it factors through the enveloping group.
-/
lemma to_envel_gp.univ (M : Type*) [monoid M] (G : Type*) [group G] (f : M →* G) :
  (to_envel_gp.map f).comp (to_envel_gp M) = f :=
by { ext, refl }

/--
The homomorphism `to_envel_gp.map f` is the unique map that fits into the commutative
triangle in `to_envel_gp.univ`.
-/
lemma to_envel_gp.univ_uniq (M : Type*) [monoid M] (G : Type*) [group G] (f : M →* G)
  (g : envel_gp M →* G) (h : f = g.comp (to_envel_gp M)) :
  g = to_envel_gp.map f :=
begin
  subst f, ext, refine quotient.ind (λ x, _) x,
  induction x,
  dunfold to_envel_gp.map, simp [to_envel_gp.map_aux, to_envel_gp],
  have hm : ⟦x_a.mul x_b⟧ = @has_mul.mul (envel_gp M) _ ⟦x_a⟧ ⟦x_b⟧ := rfl,
  rw hm, simp [x_ih_a, x_ih_b],
  have hm : ⟦x_a.inv⟧ = @has_inv.inv (envel_gp M) _ ⟦x_a⟧ := rfl,
  rw hm, simp [x_ih],
end

/-!
## Monoid actions
-/

/--
Formal expressions for a group generated by a monoid acting a type.
-/
inductive pre_envel_action (M : Type u) [monoid M] (α : Type v) : Type (max u v)
| incl (x : α) : pre_envel_action
| act (a : pre_envel_gp M) (x : pre_envel_action) : pre_envel_action

open pre_envel_action

/--
Relations for a group generated by a monoid acting on a type.
-/
inductive pre_envel_action_rel' (M : Type u) [monoid M] (α : Type v) [mul_action M α] : pre_envel_action M α → pre_envel_action M α → Type (max u v)
| refl {a : pre_envel_action M α} : pre_envel_action_rel' a a
| symm {a b : pre_envel_action M α} (h : pre_envel_action_rel' a b) : pre_envel_action_rel' b a
| trans {a b c : pre_envel_action M α} (hab : pre_envel_action_rel' a b) (hbc : pre_envel_action_rel' b c) : pre_envel_action_rel' a c
| congr_act (a a' : pre_envel_gp M) (ha : pre_envel_gp_rel' M a a') (x x' : pre_envel_action M α) (hx : pre_envel_action_rel' x x') :
  pre_envel_action_rel' (act a x) (act a' x')
| assoc (a b : pre_envel_gp M) (x : pre_envel_action M α) :
  pre_envel_action_rel' (act (mul a b) x) (act a (act b x))
| apply (m : M) (x : α) : pre_envel_action_rel' (act (incl m) (incl x)) (incl (m • x))
| one_mul (x : pre_envel_action M α) : pre_envel_action_rel' (act (incl 1) x) x

/--
The above relation as a `Prop`.
-/
inductive pre_envel_action_rel (M : Type u) [monoid M] (α : Type v) [mul_action M α] : pre_envel_action M α → pre_envel_action M α → Prop
| rel {a b : pre_envel_action M α} (r : pre_envel_action_rel' M α a b) : pre_envel_action_rel a b

def pre_envel_action_rel'.rel {M : Type u} [monoid M] {α : Type v} [mul_action M α] {a b : pre_envel_action M α} :
  pre_envel_action_rel' M α a b → pre_envel_action_rel M α a b :=
pre_envel_action_rel.rel

@[refl]
lemma pre_envel_action_rel.refl {M : Type u} [monoid M] {α : Type v} [mul_action M α] {a : pre_envel_action M α} : pre_envel_action_rel M α a a :=
pre_envel_action_rel.rel pre_envel_action_rel'.refl

@[symm]
lemma pre_envel_action_rel.symm {M : Type u} [monoid M] {α : Type v} [mul_action M α] {a b : pre_envel_action M α} :
  pre_envel_action_rel M α a b → pre_envel_action_rel M α b a
| ⟨r⟩ := r.symm.rel

@[trans]
lemma pre_envel_action_rel.trans {M : Type u} [monoid M] {α : Type v} [mul_action M α] {a b c : pre_envel_action M α} :
  pre_envel_action_rel M α a b → pre_envel_action_rel M α b c → pre_envel_action_rel M α a c
| ⟨rab⟩ ⟨rbc⟩ := (rab.trans rbc).rel

instance pre_envel_action.setoid (M : Type u) [monoid M] (α : Type v) [mul_action M α] : setoid (pre_envel_action M α) :=
{ r := pre_envel_action_rel M α,
  iseqv := begin
    split, apply pre_envel_action_rel.refl,
    split, apply pre_envel_action_rel.symm,
    apply pre_envel_action_rel.trans,
  end }

/--
The universal enveloping group action for the monoid action.
-/
def envel_action (M : Type u) [monoid M] (α : Type v) [mul_action M α] := quotient (pre_envel_action.setoid M α)

/--
Include the acted-upon set into its enveloping group action
-/
def envel_action.incl (M : Type u) [monoid M] (α : Type v) [mul_action M α] :
  α → envel_action M α :=
λ x, ⟦pre_envel_action.incl x⟧

instance envel_action.envel_mul_action (M : Type u) [monoid M] {α : Type v} [mul_action M α] : mul_action (envel_gp M) (envel_action M α) :=
{ smul := λ m x, quotient.lift_on₂ m x (λ m x, ⟦pre_envel_action.act m x⟧) (begin
    intros m x m' x' hm hx, apply quotient.sound, cases hm, cases hx,
    exact (pre_envel_action_rel'.congr_act _ _ hm_r _ _ hx_r).rel,
  end),
  one_smul := λ b, begin
    refine quotient.ind (λ b, _) b,
    apply quotient.sound, split, apply pre_envel_action_rel'.one_mul,
  end,
  mul_smul := λ a b x, begin
    refine quotient.ind (λ a, _) a,
    refine quotient.ind (λ b, _) b,
    refine quotient.ind (λ x, _) x,
    apply quotient.sound, split,
    apply pre_envel_action_rel'.assoc,
  end }

instance envel_action.mul_action (M : Type u) [monoid M] {α : Type v} [mul_action M α] : mul_action M (envel_action M α) :=
{ smul := λ m x, (to_envel_gp M m) • x,
  one_smul := by simp,
  mul_smul := begin
    intros x y b, change (to_envel_gp M (x * y)) • b = _,
    rw ←mul_smul, congr, simp,
  end }

/--
The maps `to_envel_gp` and `envel_action.incl` intertwine a monoid action.
-/
@[simp]
lemma envel_action_hom (M : Type u) [monoid M] {α : Type v} [mul_action M α] (m : M) (x : α) :
  (to_envel_gp M m) • (envel_action.incl M α x) = envel_action.incl M α (m • x) :=
begin
  convert_to _ = m • envel_action.incl M α x,
  apply quotient.sound, exact (pre_envel_action_rel'.apply m x).rel.symm,
  refl,
end

def action_induce_aux 
  (M : Type*) [monoid M] (α : Type*)
  (G : Type*) [group G] (β : Type*) [mul_action G β]
  (f : M →* G) (f' : α → β) :
  pre_envel_action M α → β
| (incl x) := f' x
| (act a b) := to_envel_gp.map_aux f a • action_induce_aux b

namespace action_induce_aux
open pre_envel_action_rel'

lemma well_def
  (M : Type*) [monoid M] (α : Type*) [mul_action M α]
  (G : Type*) [group G] (β : Type*) [mul_action G β]
  (f : M →* G) (f' : α → β) (h : ∀ (m : M) (x : α), f' (m • x) = f m • f' x) :
  Π {a b : pre_envel_action M α}, pre_envel_action_rel' M α a b → action_induce_aux M α G β f f' a = action_induce_aux M α G β f f' b
| a b refl := rfl
| a b (symm h) := (well_def h).symm
| a b (trans hac hcb) := eq.trans (well_def hac) (well_def hcb)
| _ _ (congr_act a a' ha x x' hx) := by {
  dsimp [action_induce_aux],
  rw [to_envel_gp.map_aux.well_def f ha, well_def hx], }
| _ _ (assoc a b x) := by { apply mul_smul }
| _ _ (apply m x) := by { dsimp [action_induce_aux, to_envel_gp.map_aux], simp [h] }
| _ _ (one_mul a) := by { dsimp [action_induce_aux, to_envel_gp.map_aux], simp, }

end action_induce_aux

/--
Given a monoid action and a homomorphism to a group action, induce a homomorphism from
`envel_action M α` to the group action.
This is the map for the universal property.
-/
def action_induce
  {M : Type*} [monoid M] {α : Type*} [mul_action M α]
  {G : Type*} [group G] {β : Type*} [mul_action G β]
  (f : M →* G) (f' : α → β) (h : ∀ (m : M) (x : α), f' (m • x) = f m • f' x) :
  envel_action M α → β :=
λ m, quotient.lift_on m (action_induce_aux M α G β f f')
  (λ a b ⟨hab⟩, action_induce_aux.well_def M α G β f f' h hab)

/--
Check that this indeed intertwines.
-/
lemma action_induce_is_hom
  {M : Type*} [monoid M] {α : Type*} [mul_action M α]
  {G : Type*} [group G] {β : Type*} [mul_action G β]
  (f : M →* G) (f' : α → β) (h : ∀ (m : M) (x : α), f' (m • x) = f m • f' x)
  (g : envel_gp M) (x : envel_action M α) :
  action_induce f f' h (g • x) = to_envel_gp.map f g • action_induce f f' h x :=
begin
  refine quotient.ind (λ g, _) g,
  refine quotient.ind (λ x, _) x,
  refl,
end

def quoA.rel (M : Type*) [monoid M] (α : Type*) [mul_action M α] :=
(λ (x y : α), ∃ (a : M), x = a • y)

/--
The quotient of a set by a monoid action, using `quot`.
-/
def quoA (M : Type*) [monoid M] (α : Type*) [mul_action M α]
:= quot (quoA.rel M α)


def quoB.setoid (M : Type*) [monoid M] (α : Type*) [mul_action M α] :=
mul_action.orbit_rel (envel_gp M) (envel_action M α)

/--
The quotient of a set by a monoid action, indirectly as the quotient of the
enveloping group on the corresponding enveloping action.
-/
def quoB (M : Type*) [monoid M] (α : Type*) [mul_action M α]
:= quotient (quoB.setoid M α)


def quoB.rel' (M : Type*) [monoid M] (α : Type*) [mul_action M α] :
  pre_envel_action M α → pre_envel_action M α → Prop :=
λ a b, ∃ (m : pre_envel_gp M), pre_envel_action_rel M α a (act m b)

lemma quoB.eqv (M : Type*) [monoid M] (α : Type*) [mul_action M α] (a b : pre_envel_action M α) :
  @setoid.r _ (quoB.setoid M α) (@quotient.mk _ (pre_envel_action.setoid M α) a) (@quotient.mk _ _ b)
  ↔ quoB.rel' M α a b :=
begin
  change _ ∈ _ ↔ _,
  dsimp [mul_action.orbit], dsimp [quoB.rel'], split,
  rintro ⟨g, hg⟩, dsimp at hg,
  refine quotient.ind (λ g hg, _) g hg,
  use g, exact (quotient.exact hg).symm,
  rintro ⟨g, hg⟩, use ⟦g⟧, apply quotient.sound, exact hg.symm,
end

section quoB_rel'_equiv
variables {M : Type*} [monoid M] {α : Type*} [mul_action M α]

@[refl]
def quoB.rel'.refl {a : pre_envel_action M α} : quoB.rel' M α a a :=
by { rw ←quoB.eqv, convert setoid.refl _ }

@[symm]
def quoB.rel'.symm {a b : pre_envel_action M α} : quoB.rel' M α a b → quoB.rel' M α b a :=
by { repeat { rw ←quoB.eqv }, intro h, exact @setoid.symm _ (quoB.setoid M α) _ _ h, }

@[trans]
def quoB.rel'.trans {a b c : pre_envel_action M α} : quoB.rel' M α a b → quoB.rel' M α b c → quoB.rel' M α a c :=
by { repeat { rw ←quoB.eqv }, intros h₁ h₂, exact @setoid.trans _ (quoB.setoid M α) _ _ _ h₁ h₂, }

end quoB_rel'_equiv

def quoA_to_quoB (M : Type*) [monoid M] (α : Type*) [mul_action M α] : quoA M α → quoB M α :=
λ x, quot.lift_on x (λ x, @quotient.mk _ (mul_action.orbit_rel (envel_gp M) (envel_action M α))
                            (envel_action.incl M α x)) (begin
  rintros x x' ⟨m, hm⟩,
  apply quotient.sound,
  use to_envel_gp M m,
  dsimp, simp [hm],
end)

/--
In `quoB`, two elements are related if they are related by multiplication by `envel_gp M`,
so we can strip away the action to get an equivalent term.  See `quoB.strip_action_eqv`.
-/
def quoB.strip_action (M : Type*) [monoid M] (α : Type*) [mul_action M α] : pre_envel_action M α → α
| (incl x) := x
| (act a x) := quoB.strip_action x

lemma quoB.rel'.strip (M : Type*) [monoid M] (α : Type*) [mul_action M α] (a : pre_envel_gp M) (x : pre_envel_action M α) :
  quoB.rel' M α (act a x) x :=
begin
  use a,
end

lemma quoB.rel'.strip_act (M : Type*) [monoid M] (α : Type*) [mul_action M α] (a : pre_envel_gp M) (x y : pre_envel_action M α) :
  quoB.rel' M α (act a x) y ↔ quoB.rel' M α x y :=
begin
  split, intro h, exact quoB.rel'.trans (quoB.rel'.strip M α a x).symm h,
  intro h, refine quoB.rel'.trans (quoB.rel'.strip M α a x) h,
end

lemma quoB.strip_action_eqv (M : Type*) [monoid M] (α : Type*) [mul_action M α] (a : pre_envel_action M α) :
  quoB.rel' M α a (incl (quoB.strip_action M α a)) :=
begin
  induction a,
  dsimp [quoB.strip_action], refl,
  dsimp [quoB.strip_action], rw quoB.rel'.strip_act, exact a_ih,
end

section
open pre_envel_action_rel'
lemma quoB.strip_eqv' (M : Type*) [monoid M] (α : Type*) [mul_action M α] : Π {a b : pre_envel_action M α},
  pre_envel_action_rel' M α a b → eqv_gen (quoA.rel M α) (quoB.strip_action M α a) (quoB.strip_action M α b)
| a b refl := eqv_gen.refl _
| a b (symm h) := by { apply eqv_gen.symm, apply quoB.strip_eqv' h }
| a b (trans h₁ h₂) := eqv_gen.trans _ _ _ (quoB.strip_eqv' h₁) (quoB.strip_eqv' h₂)
| _ _ (congr_act a a' ha x x' hx) := quoB.strip_eqv' hx
| _ _ (assoc a b x) := eqv_gen.refl _
| _ _ (apply m x) := by { dsimp [quoB.strip_action], apply eqv_gen.symm, apply eqv_gen.rel, use m, }
| _ _ (one_mul x) := eqv_gen.refl _
end


def quoB_to_quoA (M : Type*) [monoid M] (α : Type*) [mul_action M α] : quoB M α → quoA M α :=
λ x, quot.lift_on x (λ x', quotient.lift_on x' (λ x'', quot.mk (quoA.rel M α) (quoB.strip_action M α x'')) (begin
  intros a a' ha, cases ha, apply quot.eqv_gen_sound, apply quoB.strip_eqv', exact ha_r,
end)) (begin
  intros a a' ha, dsimp, cases ha, subst a, dsimp,
  refine quotient.ind (λ a', _) a',
  refine quotient.ind (λ ha_w, _) ha_w,
  refl,
end)


lemma quoA_equiv_quoB (M : Type*) [monoid M] (α : Type*) [mul_action M α] : quoA M α ≃ quoB M α :=
{ to_fun := quoA_to_quoB M α,
  inv_fun := quoB_to_quoA M α,
  left_inv := begin
    intro x, induction x, refl, refl,
  end,
  right_inv := begin
    intro x, refine @quotient.ind _ (quoB.setoid M α) _ (λ x, _) x,
    refine quotient.ind (λ x, _) x,
    cases x, refl,
    apply quotient.sound, change @setoid.r _ (quoB.setoid M α) _ _,
    apply (quoB.eqv M α _ _).mpr,
    dsimp [quoB.strip_action],
    refine quoB.rel'.trans _ (quoB.rel'.strip M α x_a x_x).symm,
    exact (quoB.strip_action_eqv M α x_x).symm,
  end }

@[simp]
lemma quoB_reduce (M : Type*) [monoid M] (α : Type*) [mul_action M α]
  (a : envel_gp M) (x : envel_action M α) :
  @quotient.mk _ (quoB.setoid M α) (a • x) = @quotient.mk _ (quoB.setoid M α) x :=
begin
  refine quotient.ind (λ a, _) a,
  refine quotient.ind (λ x, _) x,
  apply quotient.sound,
  change @setoid.r _ (quoB.setoid M α) _ _,
  apply (quoB.eqv M α _ _).mpr,
  apply quoB.rel'.strip,
end

@[simp]
lemma quoB_reduce_incl (M : Type*) [monoid M] (α : Type*) [mul_action M α]
  (a : M) (x : α) :
  @quotient.mk _ (quoB.setoid M α) (envel_action.incl M α (a • x)) = @quotient.mk _ (quoB.setoid M α) (envel_action.incl M α x) :=
begin
  apply quotient.sound,
  change @setoid.r _ (quoB.setoid M α) _ _,
  apply (quoB.eqv M α _ _).mpr,
  use a, exact (pre_envel_action_rel'.apply a x).symm.rel,
end

@[simp]
lemma quoA_reduce (M : Type*) [monoid M] (α : Type*) [mul_action M α]
  (m : M) (x : α) :
  (quot.mk (quoA.rel M α) (m • x)) = quot.mk _ x :=
by { apply quot.sound, use m }

/--
A little silly, but shows that the equivalence sends equivalence classes to equivalence classes.
-/
lemma quoA_equiv_quoB.hom (M : Type*) [monoid M] (α : Type*) [mul_action M α]
  (m : M) (x : α) :
  quoA_equiv_quoB M α (quot.mk (quoA.rel M α) (m • x)) = @quotient.mk _ (quoB.setoid M α) (to_envel_gp M m • envel_action.incl M α x) :=
begin
  simp, change (quoA_equiv_quoB M α).to_fun _ = _,
  delta quoA_equiv_quoB, dsimp, refl,
end