dividedPowers_unique — Mathlib

English

If hquot is a DividedPowers on the quotient I.map f and is compatible with hI via an IsDPMorphism, then hquot equals the induced dividedPowers on the quotient, i.e., the DP-structure is unique.

Русский

Пусть hquot — DP на образе I.map f; если он совместим с hI через IsDPMorphism, тогда hquot совпадает с индуцированной структурой DP на этом образе; структура DP единственна.

LaTeX

$$$hquot = DividedPowers.Quotient.OfSurjective.dividedPowers(hI, hf, hIJ, hIf)$$$

Lean4

theorem dividedPowers_unique (hquot : DividedPowers J) (hm : DividedPowers.IsDPMorphism hI hquot f) :
    hquot = dividedPowers hI hf hIJ hIf :=
  ext _ _ fun n x hx ↦ by
    obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
    rw [hm.2 a ha, dpow_apply hI hf hIJ hIf ha]

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