English
The intersection of all translates of a finite block B that contain a fixed point a is itself a block.
Русский
Пересечение всех образований блока B под действием группы G, содержащих фиксированную точку a, образует блок.
LaTeX
$$$\bigcap_{k\in G\, :\, a\in k\cdot B} k\cdot B \text{ is a Block}$$$
Lean4
/-- The intersection of the translates of a *finite* subset which contain a given point
is a block (Wielandt, th. 7.3). -/
@[to_additive /-- The intersection of the translates of a *finite* subset which contain a given point
is a block (Wielandt, th. 7.3). -/
]
theorem of_subset (a : X) (hfB : B.Finite) : IsBlock G (⋂ (k : G) (_ : a ∈ k • B), k • B) :=
by
let B' := ⋂ (k : G) (_ : a ∈ k • B), k • B
rcases Set.eq_empty_or_nonempty B with hfB_e | hfB_ne
· simp [hfB_e]
have hB'₀ : ∀ (k : G) (_ : a ∈ k • B), B' ≤ k • B := by
intro k hk
exact Set.biInter_subset_of_mem hk
have hfB' : B'.Finite := by
obtain ⟨b, hb : b ∈ B⟩ := hfB_ne
obtain ⟨k, hk : k • b = a⟩ := exists_smul_eq G b a
apply Set.Finite.subset (Set.Finite.map _ hfB) (hB'₀ k ⟨b, hb, hk⟩)
have hag : ∀ g : G, a ∈ g • B' → B' ≤ g • B' := by
intro g hg x hx
simp only [B', Set.mem_iInter, Set.mem_smul_set_iff_inv_smul_mem, smul_smul, ← mul_inv_rev] at hg hx ⊢
exact fun _ ↦ hx _ ∘ hg _
have hag' (g : G) (hg : a ∈ g • B') : B' = g • B' :=
by
rw [eq_comm, ← mem_stabilizer_iff, mem_stabilizer_set_iff_subset_smul_set hfB']
exact hag g hg
rw [isBlock_iff_smul_eq_of_nonempty]
rintro g ⟨b : X, hb' : b ∈ g • B', hb : b ∈ B'⟩
obtain ⟨k : G, hk : k • a = b⟩ := exists_smul_eq G a b
have hak : a ∈ k⁻¹ • B' := by
refine ⟨b, hb, ?_⟩
simp only [← hk, inv_smul_smul]
have hagk : a ∈ (k⁻¹ * g) • B' :=
by
rw [mul_smul, Set.mem_smul_set_iff_inv_smul_mem, inv_inv, hk]
exact hb'
have hkB' : B' = k⁻¹ • B' := hag' k⁻¹ hak
have hgkB' : B' = (k⁻¹ * g) • B' := hag' (k⁻¹ * g) hagk
rw [mul_smul] at hgkB'
rw [← smul_eq_iff_eq_inv_smul] at hkB' hgkB'
rw [← hgkB', hkB']
