forget_eq_ConcreteCategory_hom — Mathlib

English

For a category C with a forgetful functor to Type, the forgetful map agrees with the ConcreteCategory.hom from the toConcreteCategory instance.

Русский

Для категории C со скользящим функтором к Type, отображение забывания совпадает с hom из ConcreteCategory для данного экземпляра.

LaTeX

$$$ (forget C).map f = @ConcreteCategory.hom_{\text{...}} _ f $$$

Lean4

/-- Note that the `ConcreteCategory` and `HasForget` instances here differ from `forget_map_eq_coe`.
-/
theorem forget_eq_ConcreteCategory_hom [HasForget C] {X Y : C} (f : X ⟶ Y) :
    (forget C).map f = @ConcreteCategory.hom _ _ _ _ _ (HasForget.toConcreteCategory C) _ _ f := by
  with_reducible_and_instances rfl

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