Skip to content

Instantly share code, notes, and snippets.

@rwbarton
Created May 26, 2018 20:32
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save rwbarton/658ccdd57986b32fd8be0c155c63d47e to your computer and use it in GitHub Desktop.
Save rwbarton/658ccdd57986b32fd8be0c155c63d47e to your computer and use it in GitHub Desktop.
import data.equiv
universe u
structure strictification (α : Type u) [monoid α] : Type u :=
(action : α → α)
(equivariant : ∀ a b, action (a * b) = action a * b)
lemma strictification.eq {α : Type u} [monoid α] {f g : strictification α} :
f.action = g.action → f = g :=
by intro; cases f; cases g; simpa
variables {α : Type u}
instance [monoid α] : monoid (strictification α) :=
{ one := ⟨id, by intros a b; refl⟩,
mul := λ f g, ⟨f.action ∘ g.action, λ a b,
show f.action (g.action (a * b)) = f.action (g.action a) * b,
by rw [g.equivariant, f.equivariant]⟩,
mul_one := λ f, by cases f; refl,
one_mul := λ f, by cases f; refl,
mul_assoc := λ f g h, rfl }
def equiv_strictification [monoid α] : α ≃ strictification α :=
{ to_fun := λ a, ⟨(*) a, by intros; rw mul_assoc⟩,
inv_fun := λ f, f.action 1,
left_inv := λ a, by simp,
right_inv := λ f, strictification.eq $ funext $ λ a,
show f.action 1 * a = f.action a, by rw ←f.equivariant 1 a; simp }
lemma equiv_monoid_hom [monoid α] {a b : α} :
equiv_strictification.to_fun (a * b) =
equiv_strictification.to_fun a * equiv_strictification.to_fun b :=
strictification.eq $ funext $ λ c, show (a * b) * c = a * (b * c),
by rw mul_assoc
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment