isComplement_range_left — Mathlib

English

If there exists a function f: G/H → G with f(q) lifting q (i.e. Quot.mk(f q) = q), then range(f) is a complement of H in G.

Русский

Если существует отображение f: G/H → G, такое что Quot.mk(f(q)) = q, то range(f) является дополнением к H в G.

LaTeX

$$$\\text{range}(f) \\text{ is a complement of } H \\text{ in } G\\;\\text{ if }\\; \\forall q, Quot.mk (f(q)) = q$$$

Lean4

@[to_additive]
theorem isComplement_range_left {f : G ⧸ H → G} (hf : ∀ q, ↑(f q) = q) : IsComplement (range f) H :=
  by
  rw [isComplement_subgroup_right_iff_bijective]
  refine ⟨?_, fun q ↦ ⟨⟨f q, q, rfl⟩, hf q⟩⟩
  rintro ⟨-, q₁, rfl⟩ ⟨-, q₂, rfl⟩ h
  exact Subtype.ext <| congr_arg f <| ((hf q₁).symm.trans h).trans (hf q₂)

Похожие утверждения