WreathProducts.lean

def rightCosetMulAction (H : Subgroup G) :
    MulAction G (Quotient (QuotientGroup.rightRel H))

theorem rightCosetMulAction_mk_smul
    (H : Subgroup G) (g a : G) :
    letI := rightCosetMulAction H
    g • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) =
      Quotient.mk'' (a * g⁻¹) :=
  rfl

theorem rightCosetMulAction_inv_mk_smul
    (H : Subgroup G) (g a : G) :
    letI := rightCosetMulAction H
    g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) =
      Quotient.mk'' (a * g) := by
  rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ a]
  simp only [inv_inv]

theorem continuous_rightCosetMulAction_inv_smul_of_open
    (H : Subgroup G) (hH : IsOpen (H : Set G))
    [TopologicalSpace (Quotient (QuotientGroup.rightRel H))]
    [DiscreteTopology (Quotient (QuotientGroup.rightRel H))]
    (q : Quotient (QuotientGroup.rightRel H)) :
    letI := rightCosetMulAction H
    Continuous fun g : G => g⁻¹ • q := by
  rw [continuous_discrete_rng]
  intro q'
  classical
  let a : G := q.out
  let b : G := q'.out
  have hpre :
      (fun g : G => g⁻¹ • q) ⁻¹' (Set.singleton q') =
        (fun g : G => b * g⁻¹ * a⁻¹) ⁻¹' (H : Set G) := by
    ext g
    constructor
    · intro hg
      have hEq :
          (Quotient.mk'' (a * g) : Quotient (QuotientGroup.rightRel H)) =
            Quotient.mk'' b := by
        calc
          (Quotient.mk'' (a * g) : Quotient (QuotientGroup.rightRel H))
              = g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) := by
                  rw [rightCosetMulAction_inv_mk_smul (H := H) g a]
          _ = g⁻¹ • q := by rw [Quotient.out_eq' q]
          _ = q' := by
            change g⁻¹ • q = q' at hg
            exact hg
          _ = Quotient.mk'' b := by simp only [Quotient.out_eq, b]
      have hrel : QuotientGroup.rightRel H (a * g) b := Quotient.eq''.mp hEq
      simpa [mul_inv_rev, mul_assoc] using (QuotientGroup.rightRel_apply.mp hrel)
    · intro hg
      have hrel : QuotientGroup.rightRel H (a * g) b := by
        rw [QuotientGroup.rightRel_apply]
        simpa [mul_inv_rev, mul_assoc] using hg
      calc
        g⁻¹ • q = g⁻¹ • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel H)) := by
          rw [Quotient.out_eq' q]
        _ = Quotient.mk'' (a * g) := by
          rw [rightCosetMulAction_inv_mk_smul (H := H) g a]
        _ = Quotient.mk'' b := Quotient.eq''.mpr hrel
        _ = q' := Quotient.out_eq' q'
  change
    (fun g : G => g⁻¹ • q) ⁻¹'
      ({q'} : Set (Quotient (QuotientGroup.rightRel H))) =
        (fun g : G => b * g⁻¹ * a⁻¹) ⁻¹' (H : Set G) at hpre
  rw [hpre]
  exact hH.preimage ((continuous_const.mul continuous_inv).mul continuous_const)

abbrev PermutationalWreathProduct

instance instTopologicalSpacePermutationalWreathProduct :
    TopologicalSpace (PermutationalWreathProduct A S G)

def permutationalWreathProductHomeomorphProd :
    PermutationalWreathProduct A S G ≃ₜ (S → A) × G where
  toEquiv := SemidirectProduct.equivProd
  continuous_toFun := continuous_induced_dom
  continuous_invFun := by
    rw [continuous_induced_rng]
    simpa using (continuous_id : Continuous fun x : (S → A) × G => x)

theorem continuous_permutationalWreathProduct_equivProd :
    Continuous
      (SemidirectProduct.equivProd :
        PermutationalWreathProduct A S G → (S → A) × G)

theorem continuous_permutationalWreathProduct_left :
    Continuous (fun x : PermutationalWreathProduct A S G => x.left) :=
  continuous_fst.comp continuous_permutationalWreathProduct_equivProd

theorem continuous_permutationalWreathProduct_right :
    Continuous (fun x : PermutationalWreathProduct A S G => x.right) :=
  continuous_snd.comp continuous_permutationalWreathProduct_equivProd

theorem continuous_permutationalWreathProduct_left_apply (s : S) :
    Continuous (fun x : PermutationalWreathProduct A S G => x.left s) :=
  (continuous_apply s).comp continuous_permutationalWreathProduct_left

instance instT2SpacePermutationalWreathProduct [T2Space A] [T2Space G] :
    T2Space (PermutationalWreathProduct A S G)

instance instCompactSpacePermutationalWreathProduct [CompactSpace A] [CompactSpace G] :
    CompactSpace (PermutationalWreathProduct A S G)

instance instTotallyDisconnectedSpacePermutationalWreathProduct
    [TotallyDisconnectedSpace A] [TotallyDisconnectedSpace G] :
    TotallyDisconnectedSpace (PermutationalWreathProduct A S G)

def functionPrecomp (g : G) (f : S → A) : S → A

theorem functionPrecomp_apply (g : G) (f : S → A) (s : S) :
    functionPrecomp g f s = f (g⁻¹ • s)

theorem mulAutArrow_apply_eq_functionPrecomp (g : G) (f : S → A) :
    mulAutArrow (G := G) (A := S) (M := A) g f = functionPrecomp g f

theorem continuous_eval_of_discreteIndex :
    Continuous (fun p : (S → A) × S => p.1 p.2) := by
  rw [continuous_iff_continuousAt]
  intro p
  have hs :
      Prod.snd ⁻¹' ({p.2} : Set S) ∈ nhds p := by
    refine IsOpen.mem_nhds ((isOpen_discrete ({p.2} : Set S)).preimage continuous_snd) ?_
    simp only [Set.mem_preimage, Set.mem_singleton_iff]
  have hEq :
      (fun q : (S → A) × S => q.1 q.2) =ᶠ[nhds p] fun q => q.1 p.2 := by
    refine Filter.eventuallyEq_iff_exists_mem.mpr ?_
    refine ⟨Prod.snd ⁻¹' ({p.2} : Set S), hs, ?_⟩
    intro q hq
    simp only [Set.mem_preimage, Set.mem_singleton_iff] at hq
    simp only [hq]
  exact ContinuousAt.congr
    (((continuous_apply p.2).comp continuous_fst).continuousAt) hEq.symm

theorem continuous_functionPrecomp :
    Continuous (fun p : G × (S → A) => functionPrecomp p.1 p.2) := by
  refine continuous_pi ?_
  intro s
  change Continuous (fun p : G × (S → A) => p.2 (p.1⁻¹ • s))
  have h :=
    (continuous_eval_of_discreteIndex (A := A) (S := S)).comp
      (continuous_snd.prodMk
        (((continuous_inv.comp continuous_fst).smul continuous_const) :
          Continuous (fun p : G × (S → A) => p.1⁻¹ • s)))
  change Continuous (fun p : G × (S → A) => p.2 (p.1⁻¹ • s)) at h
  exact h

theorem permutationalWreathProduct_mul_left
    (x y : PermutationalWreathProduct A S G) :
    (x * y).left = x.left * functionPrecomp x.right y.left

theorem permutationalWreathProduct_inv_left
    (x : PermutationalWreathProduct A S G) :
    x⁻¹.left = functionPrecomp x.right⁻¹ x.left⁻¹

instance instContinuousMulPermutationalWreathProduct
    [ContinuousMul A] [ContinuousMul G] :
    ContinuousMul (PermutationalWreathProduct A S G) where
  continuous_mul := by
    refine continuous_induced_rng.2 ?_
    change Continuous
      (fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
        ((p.1 * p.2).left, (p.1 * p.2).right))
    have hleft :
        Continuous
          (fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
            p.1.left * functionPrecomp p.1.right p.2.left) :=
      (continuous_permutationalWreathProduct_left.comp continuous_fst).mul
        (continuous_functionPrecomp.comp
          ((continuous_permutationalWreathProduct_right.comp continuous_fst).prodMk
            (continuous_permutationalWreathProduct_left.comp continuous_snd)))
    have hright :
        Continuous
          (fun p : PermutationalWreathProduct A S G × PermutationalWreathProduct A S G =>
            p.1.right * p.2.right) :=
      (continuous_permutationalWreathProduct_right.comp continuous_fst).mul
        (continuous_permutationalWreathProduct_right.comp continuous_snd)
    simpa using hleft.prodMk hright

instance instContinuousInvPermutationalWreathProduct
    [ContinuousInv A] :
    ContinuousInv (PermutationalWreathProduct A S G) where
  continuous_inv := by
    refine continuous_induced_rng.2 ?_
    change Continuous
      (fun x : PermutationalWreathProduct A S G => (x⁻¹.left, x⁻¹.right))
    have hleft :
        Continuous
          (fun x : PermutationalWreathProduct A S G =>
            functionPrecomp x.right⁻¹ x.left⁻¹) :=
      continuous_functionPrecomp.comp
        ((continuous_permutationalWreathProduct_right.inv).prodMk
          (continuous_permutationalWreathProduct_left.inv))
    have hright :
        Continuous (fun x : PermutationalWreathProduct A S G => x.right⁻¹) :=
      continuous_permutationalWreathProduct_right.inv
    have hfun :
        (fun x : PermutationalWreathProduct A S G => (x⁻¹.left, x⁻¹.right)) =
          fun x => (functionPrecomp x.right⁻¹ x.left⁻¹, x.right⁻¹) := by
      funext x
      apply Prod.ext
      · exact permutationalWreathProduct_inv_left x
      · rfl
    rw [hfun]
    exact hleft.prodMk hright

instance instIsTopologicalGroupPermutationalWreathProduct
    [TopologicalSpace S] [DiscreteTopology S] [ContinuousSMul G S]
    [IsTopologicalGroup A] [IsTopologicalGroup G] :
    IsTopologicalGroup (PermutationalWreathProduct A S G)

def permutationalWreathProductInlContinuousHom :
    (S → A) →ₜ* PermutationalWreathProduct A S G where
  toMonoidHom := SemidirectProduct.inl
  continuous_toFun := by
    refine continuous_induced_rng.2 ?_
    change Continuous
      (fun f : S → A =>
        ((SemidirectProduct.inl f : PermutationalWreathProduct A S G).left,
          (SemidirectProduct.inl f : PermutationalWreathProduct A S G).right))
    simpa using (continuous_id.prodMk continuous_const)

def permutationalWreathProductInrContinuousHom :
    G →ₜ* PermutationalWreathProduct A S G where
  toMonoidHom := SemidirectProduct.inr
  continuous_toFun := by
    refine continuous_induced_rng.2 ?_
    change Continuous
      (fun g : G =>
        ((SemidirectProduct.inr g : PermutationalWreathProduct A S G).left,
          (SemidirectProduct.inr g : PermutationalWreathProduct A S G).right))
    simpa using (continuous_const.prodMk continuous_id)

def permutationalWreathProductRightContinuousHom :
    PermutationalWreathProduct A S G →ₜ* G where
  toMonoidHom := SemidirectProduct.rightHom
  continuous_toFun := continuous_permutationalWreathProduct_right

abbrev permutationalWreathProductRightKernel :
    Subgroup (PermutationalWreathProduct A S G)

def permutationalWreathProductInlToKernelContinuousHom :
    (S → A) →ₜ* permutationalWreathProductRightKernel (A := A) (S := S) (G := G) where
  toMonoidHom :=
    { toFun := fun f => ⟨SemidirectProduct.inl f, by simp only
        [permutationalWreathProductRightKernel, MonoidHom.mem_ker,
        SemidirectProduct.rightHom_inl]⟩
      map_one' := by
        apply Subtype.ext
        simp only [map_one, OneMemClass.coe_one]
      map_mul' := by
        intro f g
        apply Subtype.ext
        simp only [map_mul, MulMemClass.mk_mul_mk]}
  continuous_toFun :=
    by
      exact Continuous.subtype_mk
        (permutationalWreathProductInlContinuousHom (A := A) (S := S) (G := G)).continuous_toFun
        (by
          intro f
          change (permutationalWreathProductInlContinuousHom (A := A) (S := S) (G := G) f).right = 1
          rfl)

theorem permutationalWreathProductInlToKernel_bijective :
    Function.Bijective
      ((permutationalWreathProductInlToKernelContinuousHom (A := A) (S := S) (G := G)) :
        (S → A) → permutationalWreathProductRightKernel (A := A) (S := S) (G := G))

def permutationalWreathProductInlKernelContinuousMulEquiv
    [CompactSpace A] [T2Space A]
    [T2Space G] :
    (S → A) ≃ₜ* permutationalWreathProductRightKernel (A := A) (S := S) (G := G)

theorem hasOpenNormalBasisInClass_permutationalWreathProduct
    [CompactSpace A] [T2Space A] [TotallyDisconnectedSpace A]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (hForm : FiniteGroupClass.Formation C)
    (hIso : FiniteGroupClass.IsomClosed C)
    (hExt : FiniteGroupClass.ExtensionClosed C)
    [DiscreteTopology S]
    (hA : HasOpenNormalBasisInClass C A)
    (hG : HasOpenNormalBasisInClass C G) :
    HasOpenNormalBasisInClass C (PermutationalWreathProduct A S G)

theorem permutationalWreathProduct_mul_left_apply
    (x y : PermutationalWreathProduct A S G) (s : S) :
    (x * y).left s = x.left s * y.left (x.right⁻¹ • s)

theorem permutationalWreathProduct_inv_left_apply
    (x : PermutationalWreathProduct A S G) (s : S) :
    x⁻¹.left s = (x.left (x.right • s))⁻¹

theorem permutationalWreathProduct_inl_left_apply
    (f : S → A) (s : S) :
    (SemidirectProduct.inl f : PermutationalWreathProduct A S G).left s = f s

theorem permutationalWreathProduct_inr_left_apply
    (g : G) (s : S) :
    (SemidirectProduct.inr g : PermutationalWreathProduct A S G).left s = 1

theorem permutationalWreathProduct_rightHom_comp_inr :
    (SemidirectProduct.rightHom :
        PermutationalWreathProduct A S G →* G).comp SemidirectProduct.inr =
      MonoidHom.id G

def permutationalWreathProductMapFun (α : A →* B) : (S → A) →* (S → B) where
  toFun f := α ∘ f
  map_one' := by
    funext s
    simp only [Function.comp_apply, Pi.one_apply, map_one]
  map_mul' f g := by
    funext s
    simp only [Function.comp_apply, Pi.mul_apply, map_mul]

def permutationalWreathProductMapLeft (α : A →* B) :
    PermutationalWreathProduct A S G →* PermutationalWreathProduct B S G

theorem permutationalWreathProductMapLeft_left_apply
    (α : A →* B) (x : PermutationalWreathProduct A S G) (s : S) :
    (permutationalWreathProductMapLeft (S := S) (G := G) α x).left s = α (x.left s)

theorem permutationalWreathProductMapLeft_right
    (α : A →* B) (x : PermutationalWreathProduct A S G) :
    (permutationalWreathProductMapLeft (S := S) (G := G) α x).right = x.right

theorem permutationalWreathProductMapLeft_injective
    (α : A →* B) (hα : Function.Injective α) :
    Function.Injective (permutationalWreathProductMapLeft (S := S) (G := G) α)

theorem permutationalWreathProductMapLeft_surjective
    (α : A →* B) (hα : Function.Surjective α) :
    Function.Surjective (permutationalWreathProductMapLeft (S := S) (G := G) α)

theorem injective_of_permutationalWreathProductMapLeft_injective
    (α : A →* B) (s : S)
    (hα : Function.Injective (permutationalWreathProductMapLeft (S := S) (G := G) α)) :
    Function.Injective α

theorem surjective_of_permutationalWreathProductMapLeft_surjective
    (α : A →* B) (s : S)
    (hα : Function.Surjective (permutationalWreathProductMapLeft (S := S) (G := G) α)) :
    Function.Surjective α

def permutationalWreathProductMapLeftContinuous
    (α : A →ₜ* B) :
    PermutationalWreathProduct A S G →ₜ* PermutationalWreathProduct B S G where
  toMonoidHom := permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom
  continuous_toFun := by
    refine continuous_induced_rng.2 ?_
    change Continuous
      (fun x : PermutationalWreathProduct A S G =>
        ((permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).left,
          (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).right))
    have hleft :
        Continuous
          (fun x : PermutationalWreathProduct A S G =>
            (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).left) := by
      refine continuous_pi ?_
      intro s
      change Continuous (fun x : PermutationalWreathProduct A S G => α (x.left s))
      have h := α.continuous_toFun.comp
        (continuous_permutationalWreathProduct_left_apply
          (A := A) (S := S) (G := G) s)
      change Continuous (fun x : PermutationalWreathProduct A S G => α (x.left s)) at h
      exact h
    have hright :
        Continuous
          (fun x : PermutationalWreathProduct A S G =>
            (permutationalWreathProductMapLeft (S := S) (G := G) α.toMonoidHom x).right) := by
      simpa using continuous_permutationalWreathProduct_right
    exact hleft.prodMk hright

instance instMulActionRightCosetStandardEmbedding :
    MulAction G (Quotient (QuotientGroup.rightRel H))

def rightTransversalSection {T : Set G}
    (hT : Subgroup.IsComplement (H : Set G) T) :
    Quotient (QuotientGroup.rightRel H) → G

theorem rightTransversalSection_spec {T : Set G}
    (hT : Subgroup.IsComplement (H : Set G) T)
    (q : Quotient (QuotientGroup.rightRel H)) :
    Quotient.mk'' (rightTransversalSection (H := H) hT q) = q

def rightQuotientSectionCocycle
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q)
    (g : G) :
    Quotient (QuotientGroup.rightRel H) → H

def rightQuotientSectionEmbedding
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
    G →* PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G where
  toFun g := ⟨rightQuotientSectionCocycle (H := H) τ hτ g, g⟩
  map_one' := by
    apply SemidirectProduct.ext
    · funext q
      apply Subtype.ext
      simp only [rightQuotientSectionCocycle, mul_one, inv_one, one_smul, mul_inv_cancel,
  SemidirectProduct.one_left, Pi.one_apply, OneMemClass.coe_one]
    · rfl
  map_mul' g₁ g₂ := by
    apply SemidirectProduct.ext
    · funext q
      apply Subtype.ext
      simp only [rightQuotientSectionCocycle, mul_inv_rev, mul_smul, mul_assoc,
          SemidirectProduct.mk_eq_inl_mul_inr,
  permutationalWreathProduct_mul_left_apply, permutationalWreathProduct_inl_left_apply,
      SemidirectProduct.right_inl,
  inv_one, one_smul, permutationalWreathProduct_inr_left_apply, SemidirectProduct.right_inr,
      mul_one, one_mul,
  MulMemClass.mk_mul_mk, inv_mul_cancel_left]
    · rfl

theorem rightQuotientSectionEmbedding_left_apply
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q)
    (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
    (rightQuotientSectionEmbedding (H := H) τ hτ g).left q =
      rightQuotientSectionCocycle (H := H) τ hτ g q

theorem rightQuotientSectionEmbedding_right
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q)
    (g : G) :
    (rightQuotientSectionEmbedding (H := H) τ hτ g).right = g

theorem rightQuotientSectionEmbedding_rightHom
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
    (SemidirectProduct.rightHom :
        PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G →* G).comp
        (rightQuotientSectionEmbedding (H := H) τ hτ) = MonoidHom.id G

theorem rightQuotientSectionEmbedding_injective
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q) :
    Function.Injective (rightQuotientSectionEmbedding (H := H) τ hτ)

instance instMulActionRightCosetStandardEmbeddingTopological :
    MulAction G (Quotient (QuotientGroup.rightRel H))

theorem continuous_rightQuotientSectionEmbedding
    [TopologicalSpace (Quotient (QuotientGroup.rightRel H))]
    [DiscreteTopology (Quotient (QuotientGroup.rightRel H))]
    (hH : IsOpen (H : Set G))
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q)
    (hτcont : Continuous τ) :
    Continuous
      (rightQuotientSectionEmbedding (H := H) τ hτ :
        G → PermutationalWreathProduct H (Quotient (QuotientGroup.rightRel H)) G)

def wreathLeftCoordinate
    (ψ : G →* PermutationalWreathProduct A S G) (s : S) : G → A

theorem wreathLeftCoordinate_mul
    (ψ : G →* PermutationalWreathProduct A S G)
    (hψ :
      (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).comp ψ =
        MonoidHom.id G)
    (s : S) (g₁ g₂ : G) :
    wreathLeftCoordinate ψ s (g₁ * g₂) =
      wreathLeftCoordinate ψ s g₁ *
        wreathLeftCoordinate ψ (g₁⁻¹ • s) g₂

theorem wreathLeftCoordinate_inv
    (ψ : G →* PermutationalWreathProduct A S G)
    (hψ :
      (SemidirectProduct.rightHom : PermutationalWreathProduct A S G →* G).comp ψ =
        MonoidHom.id G)
    (s : S) (g : G) :
    wreathLeftCoordinate ψ s g⁻¹ =
      (wreathLeftCoordinate ψ (g • s) g)⁻¹

instance instMulActionRightCosetCoordinateRecovery :
    MulAction G (Quotient (QuotientGroup.rightRel H))

theorem wreathLeftCoordinate_eq_basepoint_of_rightQuotientSection
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q)
    (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
    (hψ :
      (SemidirectProduct.rightHom :
          PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
        MonoidHom.id G)
    (hτpure :
      ∀ q : Quotient (QuotientGroup.rightRel H),
        wreathLeftCoordinate ψ
            (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) (τ q) = 1)
    (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
    wreathLeftCoordinate ψ
        (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
        (rightQuotientSectionCocycle (H := H) τ hτ g q) =
      wreathLeftCoordinate ψ q g

def rightQuotientBasepointProjectionHom
    (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
    (hψ :
      (SemidirectProduct.rightHom :
          PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
        MonoidHom.id G) :
    H →* A where
  toFun h :=
    wreathLeftCoordinate ψ
      (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) h.1
  map_one' := by
    simp only [wreathLeftCoordinate, OneMemClass.coe_one, map_one, SemidirectProduct.one_left,
        Pi.one_apply]
  map_mul' a b := by
    change
      wreathLeftCoordinate ψ
          (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H))
          (a.1 * b.1) =
        wreathLeftCoordinate ψ
            (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) a.1 *
          wreathLeftCoordinate ψ
            (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) b.1
    rw [wreathLeftCoordinate_mul (ψ := ψ) hψ
      (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) a.1 b.1]
    have ha :
        a.1⁻¹ • (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) =
          (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) := by
      rw [rightCosetMulAction_inv_mk_smul (H := H) a.1 1]
      apply Quotient.sound'
      rw [QuotientGroup.rightRel_apply]
      simp only [one_mul, H.inv_mem a.2]
    simp only [ha]

theorem rightQuotientBasepointProjectionHom_apply_cocycle
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q)
    (ψ : G →* PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G)
    (hψ :
      (SemidirectProduct.rightHom :
          PermutationalWreathProduct A (Quotient (QuotientGroup.rightRel H)) G →* G).comp ψ =
        MonoidHom.id G)
    (hτpure :
      ∀ q : Quotient (QuotientGroup.rightRel H),
        wreathLeftCoordinate ψ
            (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) (τ q) = 1)
    (g : G) (q : Quotient (QuotientGroup.rightRel H)) :
    rightQuotientBasepointProjectionHom (H := H) ψ hψ
        (rightQuotientSectionCocycle (H := H) τ hτ g q) =
      wreathLeftCoordinate ψ q g

def wreathStabilizerProjection (s : S) :
    PermutationalWreathProduct A S (MulAction.stabilizer G s) →* A where
  toFun x := x.left s
  map_one' := rfl
  map_mul' x y := by
    have hx : x.right⁻¹ • s = s := by
      exact MulAction.mem_stabilizer_iff.mp x.right⁻¹.2
    simp only [permutationalWreathProduct_mul_left_apply, hx]

theorem wreathStabilizerProjection_apply
    (s : S) (x : PermutationalWreathProduct A S (MulAction.stabilizer G s)) :
    wreathStabilizerProjection (A := A) (G := G) s x = x.left s

theorem wreathStabilizerProjection_mapLeft
    {B : Type*} [Group B]
    (α : A →* B) (s : S)
    (x : PermutationalWreathProduct A S (MulAction.stabilizer G s)) :
    wreathStabilizerProjection (A := B) (G := G) s
        (permutationalWreathProductMapLeft
          (S := S) (G := MulAction.stabilizer G s) α x) =
      α (wreathStabilizerProjection (A := A) (G := G) s x)

theorem rightQuotientSectionEmbedding_left_basepoint_of_mem
    (τ : Quotient (QuotientGroup.rightRel H) → G)
    (hτ : ∀ q, Quotient.mk'' (τ q) = q)
    (hτ1 : τ (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) = 1)
    {g : G} (hg : g ∈ H) :
    (rightQuotientSectionEmbedding (H := H) τ hτ g).left
        (Quotient.mk'' (1 : G) : Quotient (QuotientGroup.rightRel H)) =
      ⟨g, hg⟩