English
A refinement of the Smul Diff lemma expressing a conjugation relation in the presence of normality and finite index.
Русский
Уточнение леммы Smul Diff, указывающее отношение сопряжения в условиях нормальности и конечности индекса.
LaTeX
$$smul_diff' (H) α β = ...$$
Lean4
theorem smul_diff_smul' [hH : Normal H] (g : Gᵐᵒᵖ) :
diff (MonoidHom.id H) (g • α) (g • β) =
⟨g.unop⁻¹ * (diff (MonoidHom.id H) α β : H) * g.unop,
hH.mem_comm ((congr_arg (· ∈ H) (mul_inv_cancel_left _ _)).mpr (SetLike.coe_mem _))⟩ :=
by
letI := H.fintypeQuotientOfFiniteIndex
let ϕ : H →* H :=
{ toFun := fun h =>
⟨g.unop⁻¹ * h * g.unop, hH.mem_comm ((congr_arg (· ∈ H) (mul_inv_cancel_left _ _)).mpr (SetLike.coe_mem _))⟩
map_one' := by rw [Subtype.ext_iff, coe_mk, coe_one, mul_one, inv_mul_cancel]
map_mul' := fun h₁ h₂ => by simp only [Subtype.ext_iff, coe_mul, mul_assoc, mul_inv_cancel_left] }
refine (Fintype.prod_equiv (MulAction.toPerm g).symm _ _ fun x ↦ ?_).trans (map_prod ϕ _ _).symm
simp only [ϕ, smul_apply_eq_smul_apply_inv_smul, smul_eq_mul_unop, mul_inv_rev, mul_assoc, MonoidHom.id_apply,
toPerm_symm_apply, MonoidHom.coe_mk, OneHom.coe_mk]
