English
Right cosets are in bijection with left cosets; there exists a natural equivalence between the two quotient constructions α / rightRel s and α / leftRel s.
Русский
Правые косеты взаимно однозначны с левыми косетами; существует естественное эквивалентное отображение между двумя конструкциями α / rightRel s и α / leftRel s.
LaTeX
$$Quotient (QuotientGroup.rightRel s) ≃ α ⧸ s$$
Lean4
/-- Right cosets are in bijection with left cosets. -/
@[to_additive /-- Right cosets are in bijection with left cosets. -/
]
def quotientRightRelEquivQuotientLeftRel : Quotient (QuotientGroup.rightRel s) ≃ α ⧸ s
where
toFun :=
Quotient.map' (fun g => g⁻¹) fun a b => by
rw [leftRel_apply, rightRel_apply]
exact fun h => (congr_arg (· ∈ s) (by simp)).mp (s.inv_mem h)
invFun :=
Quotient.map' (fun g => g⁻¹) fun a b => by
rw [leftRel_apply, rightRel_apply]
exact fun h => (congr_arg (· ∈ s) (by simp)).mp (s.inv_mem h)
left_inv
g :=
Quotient.inductionOn' g fun g =>
Quotient.sound'
(by
simp only [inv_inv]
exact Quotient.exact' rfl)
right_inv
g :=
Quotient.inductionOn' g fun g =>
Quotient.sound'
(by
simp only [inv_inv]
exact Quotient.exact' rfl)
