Lean4
/-- The equivalence induced by `PartialFunToPointed` and `PointedToPartialFun`.
`Part.equivOption` made functorial. -/
@[simps!]
noncomputable def partialFunEquivPointed : PartialFun.{u} ≌ Pointed
where
functor := partialFunToPointed
inverse := pointedToPartialFun
unitIso :=
NatIso.ofComponents
(fun X =>
PartialFun.Iso.mk
{ toFun := fun a => ⟨some a, some_ne_none a⟩
invFun := fun a => Option.get _ (Option.ne_none_iff_isSome.1 a.2)
left_inv := fun _ => Option.get_some _ _
right_inv := fun a => by simp only [some_get, Subtype.coe_eta] })
fun f =>
PFun.ext fun a b => by
dsimp [PartialFun.Iso.mk, CategoryStruct.comp, pointedToPartialFun]
rw [Part.bind_some]
refine (Part.mem_bind_iff.trans ?_).trans PFun.mem_toSubtype_iff.symm
obtain ⟨b | b, hb⟩ := b
· exact (hb rfl).elim
· simp only [partialFunToPointed_obj, ne_eq, Part.mem_some_iff, Subtype.mk.injEq, some.injEq, exists_eq_right',
elim'_some]
classical
refine Part.mem_toOption.symm.trans ?_
exact eq_comm
counitIso :=
NatIso.ofComponents (fun X ↦ Pointed.Iso.mk (by classical exact Equiv.optionSubtypeNe X.point) (by rfl))
fun {X Y} f ↦
Pointed.Hom.ext <|
funext fun a ↦ by
obtain _ | ⟨a, ha⟩ := a
· exact f.map_point.symm
simp_all [Option.casesOn'_eq_elim, Part.elim_toOption]
functor_unitIso_comp
X := by
ext (_ | x)
· rfl
· simp
rfl
