English
There is a natural equivalence between the quotient of the subgroup action on an orbit and the quotient setoid derived via comap Subtype.val.
Русский
Существует естественное эквивалентное отображение между фактор-обществом подгруппы в орбите и фактор-объединением через сопоставление Subtype.val.
LaTeX
$$orbitRel.Quotient H (orbitRel.Quotient.orbit ω) ≃ Quotient ((orbitRel H β).comap (Subtype.val ...))$$
Lean4
/-- A bijection between the quotient of the action of a subgroup `H` on an orbit, and a
corresponding quotient expressed in terms of `Setoid.comap Subtype.val`. -/
@[to_additive /-- A bijection between the quotient of the action of an additive subgroup `H` on an
orbit, and a corresponding quotient expressed in terms of `Setoid.comap Subtype.val`. -/
]
noncomputable def equivSubgroupOrbitsSetoidComap (H : Subgroup α) (ω : Ω) :
orbitRel.Quotient H (orbitRel.Quotient.orbit ω) ≃
Quotient ((orbitRel H β).comap (Subtype.val : Quotient.mk (orbitRel α β) ⁻¹' { ω } → β))
where
toFun := fun q ↦
q.liftOn'
(fun x ↦
⟦⟨↑x, by
simp only [Set.mem_preimage, Set.mem_singleton_iff]
have hx := x.property
rwa [orbitRel.Quotient.mem_orbit] at hx⟩⟧)
fun a b h ↦ by
simp only [← Quotient.eq, orbitRel.Quotient.subgroup_quotient_eq_iff] at h
simp only [Quotient.eq] at h ⊢
exact h
invFun := fun q ↦
q.liftOn'
(fun x ↦
⟦⟨↑x, by
have hx := x.property
simp only [Set.mem_preimage, Set.mem_singleton_iff] at hx
rwa [orbitRel.Quotient.mem_orbit, @Quotient.mk''_eq_mk]⟩⟧)
fun a b h ↦ by
rw [Setoid.comap_rel, ← Quotient.eq'', @Quotient.mk''_eq_mk] at h
simp only [orbitRel.Quotient.subgroup_quotient_eq_iff]
exact h
left_inv := by
simp only [LeftInverse]
intro q
induction q using Quotient.inductionOn'
rfl
right_inv := by
simp only [Function.RightInverse, LeftInverse]
intro q
induction q using Quotient.inductionOn'
rfl
