English
For a finite-index subgroup H of a group G and a homomorphism ϕ from H to a commutative group A, the quantity diff(ϕ, R, S) measures how two left transversals R and S differ. It satisfies an associativity-type rule: diff(ϕ, R, S) · diff(ϕ, S, T) = diff(ϕ, R, T); diff(ϕ, S, S) = 1; and the inverse relation diff(ϕ, S, T)^{-1} = diff(ϕ, T, S).
Русский
Для конечного по индексу подгруппы H группы G и гомоморфизма ϕ: H →* A в коммутативную группу A величина diff(ϕ, R, S) измеряет различие между двумя левыми трансверсалями R и S. Она удовлетворяет тождественности типа ассоциативности: diff(ϕ, R, S) · diff(ϕ, S, T) = diff(ϕ, R, T); diff(ϕ, S, S) = 1; и diff(ϕ, S, T)^{-1} = diff(ϕ, T, S).
LaTeX
$$$\operatorname{diff}(\varphi,R,S) \cdot \operatorname{diff}(\varphi,S,T) = \operatorname{diff}(\varphi,R,T) \;\land\; \operatorname{diff}(\varphi,S,S) = 1 \;\land\; (\operatorname{diff}(\varphi,S,T))^{-1} = \operatorname{diff}(\varphi,T,S)$$$
Lean4
/-- The difference of two left transversals -/
@[to_additive /-- The difference of two left transversals -/
]
noncomputable def diff : A :=
let α := S.2.leftQuotientEquiv
let β := T.2.leftQuotientEquiv
let _ := H.fintypeQuotientOfFiniteIndex
∏ q : G ⧸ H,
ϕ
⟨(α q : G)⁻¹ * β q,
QuotientGroup.leftRel_apply.mp <| Quotient.exact' ((α.symm_apply_apply q).trans (β.symm_apply_apply q).symm)⟩
