Skip to content

Instantly share code, notes, and snippets.

@ChrisHughes24

ChrisHughes24/coprodEquivSemidirectProduct

Created September 8, 2023 10:43
Show Gist options
  • Save ChrisHughes24/67ef769231fefab346751c7b76fed01c to your computer and use it in GitHub Desktop.
Save ChrisHughes24/67ef769231fefab346751c7b76fed01c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
coprodEquivSemidirectProduct
open Monoid Monoid.Coprod SemidirectProduct
-- def Monoid.CoprodI.mapEquivHom (ι M : Type*) [Monoid M] :
-- Equiv.Perm ι →* MulAut (Monoid.CoprodI (fun _ : ι => M)) :=
-- { toFun := fun e =>
-- MonoidHom.toMulEquiv
-- (Monoid.CoprodI.lift (fun i =>
-- CoprodI.of (M := fun _ : ι => M) (i := e i)))
-- (Monoid.CoprodI.lift (fun i =>
-- CoprodI.of (M := fun _ : ι => M) (i := e.symm i)))
-- (CoprodI.ext_hom _ _ (fun _ => by ext; simp))
-- (CoprodI.ext_hom _ _ (fun _ => by ext; simp))
-- map_one' := MulEquiv.toMonoidHom_injective
-- (CoprodI.ext_hom _ _ (fun _ => by ext; simp))
-- map_mul' := fun _ _ => MulEquiv.toMonoidHom_injective
-- (CoprodI.ext_hom _ _ (fun _ => by ext; simp)) }
-- @[simp] theorem Monoid.CoprodI.mapEquivHom_of (ι M : Type*) [Monoid M]
-- (e : Equiv.Perm ι) (i : ι) (m : M) :
-- Monoid.CoprodI.mapEquivHom ι M e (CoprodI.of (M := fun _ : ι => M) (i := i) m) =
-- CoprodI.of (M := fun _ : ι => M) (i := e i) m := by
-- simp [Monoid.CoprodI.mapEquivHom]
-- def coprodEquivSemidirectProduct (G H : Type*) [Group G] [Group H] :
-- (G ∗ H) ≃* Monoid.CoprodI (fun _ : H => G)
-- ⋊[(CoprodI.mapEquivHom H G).comp (MulAction.toPermHom _ _)] H :=
-- MonoidHom.toMulEquiv
-- (Coprod.lift
-- (inl.comp (CoprodI.of (M := fun _ : H => G) (i := 1)))
-- inr)
-- (SemidirectProduct.lift
-- (CoprodI.lift (fun h : H => (MulAut.conj (Coprod.inr h)).toMonoidHom.comp
-- Coprod.inl))
-- inr
-- (fun h => CoprodI.ext_hom _ _
-- (fun h₂ => by ext; simp [CoprodI.mapEquivHom])))
-- (Coprod.ext_hom _ _ (by ext; simp) (by ext; simp))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment