equivalenceMonoOver — Mathlib

English

For A a subpresheaf, range of Subobject.mk A.ι .arrow equals A.

Русский

Для A—подпрефеш, range от Subobject.mk A.ι .arrow равно A.

LaTeX

$$$\\mathrm{range}(\\mathrm{Subobject.mk} A.\\iota).\\mathrm{arrow} = A$$$

Lean4

/-- The equivalence of categories `Subpresheaf F ≌ MonoOver F`. -/
@[simps]
noncomputable def equivalenceMonoOver : Subpresheaf F ≌ MonoOver F
    where
  functor :=
    { obj A := MonoOver.mk' A.ι
      map {A B} f := MonoOver.homMk (Subpresheaf.homOfLe (leOfHom f)) }
  inverse :=
    { obj X := Subpresheaf.range X.arrow
      map {X Y}
        f :=
        homOfLE
          (by
            rw [← MonoOver.w f]
            apply range_comp_le) }
  unitIso := NatIso.ofComponents (fun A ↦ eqToIso (by simp))
  counitIso := NatIso.ofComponents (fun X ↦ MonoOver.isoMk ((asIso (toRange X.arrow)).symm))

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