functorPushforward_id — Mathlib

English

Pushforward along the identity functor is the identity on sieves: R.functorPushforward (Id) = R.

Русский

Pushforward вдоль тождественного функторa равен тождественному на ситах.

LaTeX

$$$ R.functorPushforward (\\mathrm{Id}) = R $$$

Lean4

@[simp]
theorem functorPushforward_id (R : Sieve X) : R.functorPushforward (𝟭 _) = R :=
  by
  ext X f
  constructor
  · intro hf
    obtain ⟨X, g, h, hg, rfl⟩ := hf
    exact R.downward_closed hg h
  · intro hf
    exact ⟨X, f, 𝟙 _, hf, by simp⟩

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