English
Let H be a subgroup of G acting on X, and B ⊆ X a block for H. For any g ∈ G, the image of H under conjugation by g, together with the translate g +ᵥ B, forms a block: IsBlock (H.map (AddAut.conj g).toMul.toAddMonoidHom) (g +ᵥ B).
Русский
Пусть H — подгруппа G, действующая на X, B ⊆ X — блок для H. При любом g ∈ G образ H по сопряжению g образуется подгруппой; трансляция g +ᵥ B образует блок: IsBlock (H.map (AddAut.conj g).toMul.toAddMonoidHom) (g +ᵥ B).
LaTeX
$$$IsBlock(H, B) \\Rightarrow IsBlock\\left(H.map(AddAut.conj(g).toMul.toAddMonoidHom),\, g +\\!ᵥ B\\right)$$
Lean4
theorem _root_.AddAction.IsBlock.of_addSubgroup_of_conjugate {G : Type*} [AddGroup G] {X : Type*} [AddAction G X]
{B : Set X} {H : AddSubgroup G} (hB : AddAction.IsBlock H B) (g : G) :
AddAction.IsBlock (H.map (AddAut.conj g).toMul.toAddMonoidHom) (g +ᵥ B) :=
by
rw [AddAction.isBlock_iff_vadd_eq_or_disjoint]
intro h'
obtain ⟨h, hH, hh⟩ := AddSubgroup.mem_map.mp (SetLike.coe_mem h')
simp only [AddEquiv.coe_toAddMonoidHom, AddAut.conj_apply] at hh
suffices h' +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by
simp only [this]
apply (hB.vadd_eq_or_disjoint ⟨h, hH⟩).imp
· intro hB'; congr
· exact Set.disjoint_image_of_injective (AddAction.injective g)
suffices (h' : G) +ᵥ (g +ᵥ B) = g +ᵥ (h +ᵥ B) by exact this
rw [← hh, vadd_vadd, vadd_vadd]
simp
