ofQuotientStabilizer — Mathlib

English

There is a canonical map from the quotient stabilizer to the underlying set given by g ↦ g • x.

Русский

Существует каноническая карта из факторного стабилизатора в исходное множество: g ↦ g • x.

LaTeX

$$$\\operatorname{ofQuotientStabilizer}(\\alpha,x): (\\alpha \\!\\slash \\operatorname{stabilizer}(\\alpha,x)) \\to \\beta,\\; g \\mapsto g \\cdot x$$$

Lean4

/-- The canonical map from the quotient of the stabilizer to the set. -/
@[to_additive /-- The canonical map from the quotient of the stabilizer to the set. -/
    ]
def ofQuotientStabilizer (g : α ⧸ MulAction.stabilizer α x) : β :=
  Quotient.liftOn' g (· • x) fun g1 g2 H =>
    calc
      g1 • x = g1 • (g1⁻¹ * g2) • x := congr_arg _ (leftRel_apply.mp H).symm
      _ = g2 • x := by rw [smul_smul, mul_inv_cancel_left]

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