English
If H ≤ K, there is an embedding α/ s → α/ t × t/ s.subgroupOf t, built from a right inverse.
Русский
Если H ≤ K, существует вложение α/ s ↪ α/ t × t/ s.subgroupOf t, сконструированное через правый обратный.
LaTeX
$$$(H \le t) \Rightarrow \alpha/ s \hookrightarrow (\alpha/ t) \times (t/ s/ t)$$$
Lean4
/-- If `H ≤ K`, then `G/H ≃ G/K × K/H` constructively, using the provided right inverse
of the quotient map `G → G/K`. The classical version is `Subgroup.quotientEquivProdOfLE`. -/
@[to_additive (attr := simps) quotientEquivProdOfLE' /--
If `H ≤ K`, then `G/H ≃ G/K × K/H` constructively, using the provided right inverse
of the quotient map `G → G/K`. The classical version is `AddSubgroup.quotientEquivProdOfLE`. -/
]
def quotientEquivProdOfLE' (h_le : s ≤ t) (f : α ⧸ t → α) (hf : Function.RightInverse f QuotientGroup.mk) :
α ⧸ s ≃ (α ⧸ t) × t ⧸ s.subgroupOf t
where
toFun
a :=
⟨a.map' id fun _ _ h => leftRel_apply.mpr (h_le (leftRel_apply.mp h)),
a.map' (fun g : α => ⟨(f (Quotient.mk'' g))⁻¹ * g, leftRel_apply.mp (Quotient.exact' (hf g))⟩) fun b c h =>
by
rw [leftRel_apply]
change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s
have key : f b = f c := congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]⟩
invFun
a := by
refine
a.2.map' (fun (b : { x // x ∈ t }) => f a.1 * b) fun b c h =>
by
rw [leftRel_apply] at h ⊢
change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
left_inv := by
refine Quotient.ind' fun a => ?_
simp_rw [Quotient.map'_mk'', id, mul_inv_cancel_left]
right_inv := by
refine Prod.rec ?_
refine Quotient.ind' fun a => ?_
refine Quotient.ind' fun b => ?_
have key : Quotient.mk'' (f (Quotient.mk'' a) * b) = Quotient.mk'' a :=
(QuotientGroup.mk_mul_of_mem (f a) b.2).trans (hf a)
simp_rw [Quotient.map'_mk'', id, key, inv_mul_cancel_left]
