functorOp — Mathlib

English

Given a LightProfinite cone c, each projection map c.asLimitCone.π.app i is epi.

Русский

Для конуса c в LightProfinite проекции c.asLimitCone.π.app i являются эпиморфизмами.

LaTeX

$$$\\forall i, \\text{Epi} (c.asLimitCone.π.app i)$$$

Lean4

/-- Given a sequential cone in `LightProfinite` consisting of finite sets,
we obtain a functor from the opposite of the indexing category to
`CostructuredArrow toProfinite.op ⟨c.pt⟩`.
-/
@[simps! obj map]
def functorOp : ℕ ⥤ CostructuredArrow toLightProfinite.op ⟨c.pt⟩ :=
  (functor c).rightOp ⋙
    StructuredArrow.toCostructuredArrow _
      _
        -- We check that the opposite of the original diagram factors through `Profinite.Extend.functorOp`.

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