English
For subgroups H,K, the orbit relation for H.subgroupOf K equals that for H ∩ K.
Русский
Для подгрупп H и K орбитальная связь H.subgroupOf K равна орбитальной связи H ∩ K.
LaTeX
$$orbitRel (H.subgroupOf K) α = orbitRel (H ⊓ K) α$$
Lean4
@[to_additive]
theorem orbitRel_subgroupOf (H K : Subgroup G) : orbitRel (H.subgroupOf K) α = orbitRel (H ⊓ K : Subgroup G) α :=
by
rw [← Subgroup.subgroupOf_map_subtype]
ext x
simp_rw [orbitRel_apply]
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
· rcases h with ⟨⟨gv, gp⟩, rfl⟩
simp only
refine mem_orbit _ (⟨gv, ?_⟩ : Subgroup.map K.subtype (H.subgroupOf K))
simpa using gp
· rcases h with ⟨⟨gv, gp⟩, rfl⟩
simp only
simp only [Subgroup.subgroupOf_map_subtype, Subgroup.mem_inf] at gp
refine mem_orbit _ (⟨⟨gv, ?_⟩, ?_⟩ : H.subgroupOf K)
· exact gp.2
· simp only [Subgroup.mem_subgroupOf]
exact gp.1
