strictUniversalPropertyFixedTargetId

English

If W consists of isomorphisms, the identity functor satisfies the universal property of localization.

Русский

Если W состоит из изоморфизмов, тождественный функтор удовлетворяет универсальному свойству локализации.

LaTeX

$$$StrictUniversalPropertyFixedTarget\\ id\\ W E$$$

Lean4

/-- When `W` consists of isomorphisms, the identity satisfies the universal property
of the localization. -/
@[simps]
def strictUniversalPropertyFixedTargetId (hW : W ≤ MorphismProperty.isomorphisms C) :
    StrictUniversalPropertyFixedTarget (𝟭 C) W E
    where
  inverts _ _ f hf := hW f hf
  lift F _ := F
  fac F
    hF := by
    cases F
    rfl
  uniq F₁ F₂
    eq := by
    cases F₁
    cases F₂
    exact eq

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