English
The category MonoOver α is equivalent to the set-valued reindexing Set α, i.e., MonoOver α ≃ Set α.
Русский
Категория MonoOver α эквивалентна множеству α, то есть MonoOver α ≃ Set α.
LaTeX
$$$\mathrm{MonoOver}(\alpha) \simeq \mathrm{Set}(\alpha).$$$
Lean4
/-- The category of `MonoOver α`, for `α : Type u`, is equivalent to the partial order `Set α`.
-/
@[simps]
noncomputable def monoOverEquivalenceSet (α : Type u) : MonoOver α ≌ Set α
where
functor :=
{ obj := fun f => Set.range f.1.hom
map := fun {f g} t =>
homOfLE
(by
rintro a ⟨x, rfl⟩
exact ⟨t.1 x, congr_fun t.w x⟩) }
inverse :=
{ obj := fun s => MonoOver.mk' (Subtype.val : s → α)
map := fun {s t} b => MonoOver.homMk (fun w => ⟨w.1, Set.mem_of_mem_of_subset w.2 b.le⟩) }
unitIso :=
NatIso.ofComponents fun f => MonoOver.isoMk (Equiv.ofInjective f.1.hom ((mono_iff_injective _).mp f.2)).toIso
counitIso := NatIso.ofComponents fun _ => eqToIso Subtype.range_val
