functorPushforward_top — Mathlib

English

For any functor F, the pushforward of the top sieve is the top sieve: F_*(⊤) = ⊤.

Русский

Для любого функторa F перенос верхней щели равен верхней щели: F_*(⊤) = ⊤.

LaTeX

$$$F_*(\\top) = \\top$$$

Lean4

@[simp]
theorem functorPushforward_top (F : C ⥤ D) (X : C) : (⊤ : Sieve X).functorPushforward F = ⊤ :=
  by
  refine (generate_sieve _).symm.trans ?_
  apply generate_of_contains_isSplitEpi (𝟙 (F.obj X))
  exact ⟨X, 𝟙 _, 𝟙 _, trivial, by simp⟩

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