groupEquivQuotientProdSubgroup — Mathlib

English

There exists a noncanonical bijection between a group G and the product (G/s) × s.

Русский

Существует неконкретная биекция между группой G и произведением (G/s) × s.

LaTeX

$$$\;G \;\cong\; (G / s) \times s$$$

Lean4

/-- A (non-canonical) bijection between a group `α` and the product `(α/s) × s` -/
@[to_additive addGroupEquivQuotientProdAddSubgroup /--
    A (non-canonical) bijection between an add_group `α` and the product `(α/s) × s` -/
    ]
noncomputable def groupEquivQuotientProdSubgroup : α ≃ (α ⧸ s) × s :=
  calc
    α ≃ Σ L : α ⧸ s, { x : α // (x : α ⧸ s) = L } := (Equiv.sigmaFiberEquiv QuotientGroup.mk).symm
    _ ≃ Σ L : α ⧸ s, (Quotient.out L • s : Set α) :=
      (Equiv.sigmaCongrRight fun L => by
        rw [← eq_class_eq_leftCoset]
        change
          (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃
            _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _
        simp
        rfl)
    _ ≃ Σ _L : α ⧸ s, s := (Equiv.sigmaCongrRight fun _ => leftCosetEquivSubgroup _)
    _ ≃ (α ⧸ s) × s := Equiv.sigmaEquivProd _ _

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