homEquiv_eq — Mathlib

English

There is an isomorphism between the mono over m and the object representing the pullback along χ m of Ω₀.

Русский

Существует изоморфизм между MonoOver.mk' m и представителем подмножества, соответствующим вытягиванием χ m через Ω₀.

LaTeX

$$Iso (MonoOver.mk' m) (Subobject.representative.obj ((Subobject.pullback (h.χ m)).obj h.Ω₀))$$

Lean4

/-- `h.homEquiv` acts like an "object comprehension" operator: it maps any characteristic map
`f : X ⟶ Ω` to the associated subobject of `X`, obtained by pulling back `h.Ω₀` along `f`. -/
theorem homEquiv_eq {X : C} (f : X ⟶ Ω) : h.homEquiv f = (Subobject.pullback f).obj h.Ω₀ := by
  simpa using h.homEquiv_comp f (𝟙 _)

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