instEssSurjαCategoryObjLocallyDiscreteOppositeCatMkOpFiberForgetInducedFunctor

English

The instance asserts that the induced functor on objects in LocallyDiscrete Opposite 𝒮 is an equivalence.

Русский

Инстанс утверждает, что индуцированный функтор на объекте в LocallyDiscrete Opposite 𝒮 является эквивалентностью.

LaTeX

$$$(\\operatorname{inducedFunctor} (\\mathrm{comp\\_const} F S)).IsEquivalence$$$

Lean4

noncomputable instance : (Fiber.inducedFunctor (comp_const F S)).EssSurj :=
  by
  apply essSurj_of_surj
  intro Y
  have hYS : (fiberInclusion.obj Y).base = S := by simpa using Y.2
  use hYS ▸ (fiberInclusion.obj Y).fiber
  apply fiberInclusion_obj_inj
  ext <;> simp [hYS]

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