transferTransversal — Mathlib

English

The left-quotient data for the transversal recovers the transferFunction value via a canonical equivalence.

Русский

Данные левой квотентной эквивалентности трансверсали восстанавливают transferFunction через каноническое эквивалентное отображение.

LaTeX

$$$\uparrow\bigl((\mathrm{transferTransversal}(H,g)).2.leftQuotientEquiv q\bigr) = \mathrm{transferFunction}(H,g,q)$$$

Lean4

/-- The transfer transversal. Contains elements of the form `g ^ k • g₀` for fixed choices
  of representatives `g₀` of fixed choices of representatives `q₀` of `⟨g⟩`-orbits in `G ⧸ H`. -/
def transferTransversal : H.LeftTransversal :=
  ⟨transferSet H g, isComplement_range_left (coe_transferFunction g)⟩

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