English
If the action is pretransitive, then the trivial blocks condition implies preprimitivity (based condition).
Русский
Если действие предпереводимо, условие тривиальных блоков приводит к предпримитивности (базовое условие).
LaTeX
$$theorem of_isTrivialBlock_base [IsPretransitive G X] (a : X) (H : ∀ {B : Set X} (_ : a ∈ B) (_ : IsBlock G B), IsTrivialBlock B) : IsPreprimitive G X$$
Lean4
/-- If the action is not trivial, then the trivial blocks condition implies preprimitivity
(pretransitivity is automatic) (based condition) -/
@[to_additive /-- If the action is not trivial, then the trivial blocks condition implies preprimitivity
(pretransitivity is automatic) (based condition) -/
]
theorem of_isTrivialBlock_of_notMem_fixedPoints {a : X} (ha : a ∉ fixedPoints G X)
(H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B) : IsPreprimitive G X :=
have : IsPretransitive G X := by
rw [isPretransitive_iff_base a]
rcases H (mem_orbit_self a) (IsBlock.orbit a) with H | H
· exfalso; apply ha
rw [Set.subsingleton_iff_singleton (mem_orbit_self a)] at H
simp only [mem_fixedPoints]
intro g
rw [← Set.mem_singleton_iff]; rw [← H]
exact mem_orbit a g
· intro x; rw [← MulAction.mem_orbit_iff, H]; exact Set.mem_univ x
{
isTrivialBlock_of_isBlock {B}
hB := by
obtain rfl | ⟨b, hb⟩ := B.eq_empty_or_nonempty
· simp [IsTrivialBlock]
· obtain ⟨g, hg⟩ := exists_smul_eq G b a
rw [← IsTrivialBlock.smul_iff g]
exact H ⟨b, hb, hg⟩ (hB.translate g) }
