English
For a set U ⊆ α, pushing U to the quotient and pulling back yields the union of all G-translates of U.
Русский
Для множества U ⊆ α его образ в фактор-множество по орбитам и обратное изображение дают объединение всех переносов U по действию G.
LaTeX
$$$\Quotient.mk'^{-1}'(\Quotient.mk'' '' U) = \bigcup_{g \in G} (g \cdot)'' U$$$
Lean4
/-- When you take a set `U` in `α`, push it down to the quotient, and pull back, you get the union
of the orbit of `U` under `G`. -/
@[to_additive /-- When you take a set `U` in `α`, push it down to the quotient, and pull back, you get the union
of the orbit of `U` under `G`. -/
]
theorem quotient_preimage_image_eq_union_mul (U : Set α) :
letI := orbitRel G α
Quotient.mk' ⁻¹' (Quotient.mk' '' U) = ⋃ g : G, (g • ·) '' U :=
by
letI := orbitRel G α
set f : α → Quotient (MulAction.orbitRel G α) := Quotient.mk'
ext a
constructor
· rintro ⟨b, hb, hab⟩
obtain ⟨g, rfl⟩ := Quotient.exact hab
rw [Set.mem_iUnion]
exact ⟨g⁻¹, g • a, hb, inv_smul_smul g a⟩
· intro hx
rw [Set.mem_iUnion] at hx
obtain ⟨g, u, hu₁, hu₂⟩ := hx
rw [Set.mem_preimage, Set.mem_image]
refine ⟨g⁻¹ • a, ?_, by simp [f, orbitRel, Quotient.eq']⟩
rw [← hu₂]
convert hu₁
simp only [inv_smul_smul]
