instEssSurjLightDiagram'LightDiagramToLightFunctor

English

The functor LightDiagram'.toLightFunctor is essentially surjective.

Русский

Функтор LightDiagram'.toLightFunctor является по существу сюръективным (эссентуально сюръективен).

LaTeX

$$$\text{LightDiagram'.toLightFunctor}$ is essentially surjective.$$

Lean4

instance : LightDiagram'.toLightFunctor.{u}.EssSurj where
  mem_essImage
    Y :=
    ⟨⟨Y.diagram ⋙ Skeleton.equivalence.inverse⟩,
      ⟨lightDiagramToProfinite.preimageIso
          ((Limits.lim.mapIso
              (Functor.isoWhiskerRight ((Functor.isoWhiskerLeft Y.diagram Skeleton.equivalence.counitIso))
                toProfinite)) ≪≫
            (limit.isLimit _).conePointUniqueUpToIso Y.isLimit)⟩⟩

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