quotientEquiv — Mathlib

English

There is a canonical bijection between the quotient of E by the lattice spanℤ(range b) and the fundamental domain of b.

Русский

Существуют каноническая биекция между частным пространством E по подгруппе-решетке spanℤ(range b) и фундаментальной областью b.

LaTeX

$$$(E \ / \operatorname{span}_{\mathbb{Z}}(\operatorname{range} b)) \cong \operatorname{fundamentalDomain}(b).$$$

Lean4

/-- The map `ZSpan.fractRestrict` defines an equiv map between `E ⧸ span ℤ (Set.range b)`
and `ZSpan.fundamentalDomain b`. -/
def quotientEquiv [Fintype ι] : E ⧸ span ℤ (Set.range b) ≃ (fundamentalDomain b) :=
  by
  refine Equiv.ofBijective ?_ ⟨fun x y => ?_, fun x => ?_⟩
  · refine fun q => Quotient.liftOn q (fractRestrict b) (fun _ _ h => ?_)
    rw [Subtype.mk.injEq, fractRestrict_apply, fractRestrict_apply, fract_eq_fract]
    exact QuotientAddGroup.leftRel_apply.mp h
  · refine Quotient.inductionOn₂ x y (fun _ _ hxy => ?_)
    rw [Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fractRestrict,
      Quotient.liftOn_mk (s := quotientRel (span ℤ (Set.range b))), fractRestrict, Subtype.mk.injEq] at hxy
    apply Quotient.sound'
    rwa [QuotientAddGroup.leftRel_apply, mem_toAddSubgroup, ← fract_eq_fract]
  · obtain ⟨a, rfl⟩ := fractRestrict_surjective b x
    exact ⟨Quotient.mk'' a, rfl⟩

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