pullback_homEquiv_symm_obj_Ω₀ — Mathlib

English

For any X and x ∈ Subobject X, the pullback of h.homEquiv.symm x along h.Ω₀ equals x.

Русский

Для произвольного X и подобъекта x ∈ Subobject X вытягивание h.homEquiv.symm x через h.Ω₀ возвращает x.

LaTeX

$$$(Subobject.pullback (h.homEquiv.symm x)).obj h.Ω_0 = x$$$

Lean4

/-- For any subobject `x`, the pullback of `h.Ω₀` along the characteristic map of `x`
given by `h.homEquiv` is `x` itself. -/
theorem pullback_homEquiv_symm_obj_Ω₀ {X : C} (x : Subobject X) :
    (Subobject.pullback (h.homEquiv.symm x)).obj h.Ω₀ = x := by rw [← homEquiv_eq, Equiv.apply_symm_apply]

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