English
If H ⊆ G is a subgroup and B ⊆ X is a block for H, then for any g ∈ G, the set g • B is a block for the conjugate subgroup H^g.
Русский
Если H — подгруппа G и B ⊆ X — блок для H, то для любого g ∈ G множество g • B является блоком для сопряжённой подгруппы H^g.
LaTeX
$$$IsBlock(G,B) \\Rightarrow IsBlock(\\text{H}^{g}, g \\cdot B)$$$
Lean4
theorem of_subgroup_of_conjugate {H : Subgroup G} (hB : IsBlock H B) (g : G) :
IsBlock (H.map (MulAut.conj g).toMonoidHom) (g • B) :=
by
rw [isBlock_iff_smul_eq_or_disjoint]
intro h'
obtain ⟨h, hH, hh⟩ := Subgroup.mem_map.mp (SetLike.coe_mem h')
simp only [MulEquiv.coe_toMonoidHom, MulAut.conj_apply] at hh
suffices h' • g • B = g • h • B by
simp only [this]
apply (hB.smul_eq_or_disjoint ⟨h, hH⟩).imp
· intro; congr
· exact Set.disjoint_image_of_injective (MulAction.injective g)
suffices (h' : G) • g • B = g • h • B by rw [← this]; rfl
rw [← hh, smul_smul (g * h * g⁻¹) g B, smul_smul g h B, inv_mul_cancel_right]
