ofSection_eq_range — Mathlib

English

For any x ∈ F.obj X, the subpresheaf ofSection x is equal to the range of yoneda equivalence applied to x.

Русский

Для любого x ∈ F.obj X, подпрефеш ofSection x равен диапазону yoneda эквивалентности примененной к x.

LaTeX

$$$ ofSection x = range (yonedaEquiv.\\mathrm{symm}\\ x ) $$$

Lean4

theorem ofSection_eq_range {X : Cᵒᵖ} (x : F.obj X) : ofSection x = range (yonedaEquiv.symm x) :=
  by
  ext U y
  simp only [ofSection_obj, Set.mem_setOf_eq, Opposite.op_unop, range_obj, yoneda_obj_obj, Set.mem_range]
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f.unop, rfl⟩
  · rintro ⟨f, rfl⟩
    exact ⟨f.op, rfl⟩

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