instFunLikeHomSubtypeV — Mathlib

English

HomSubtype carries a FunLike structure, so HomSubtype V G M N behaves like a set of arrows with a compatible action.

Русский

HomSubtype обладает структурой FunLike, поэтому он ведет себя как множество стрелок с согласованной структурой действия.

LaTeX

$$instance: FunLike (HomSubtype V G M N) (CV M.V) (CV N.V)$$

Lean4

instance {FV : V → V → Type*} {CV : V → Type*} [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)] [ConcreteCategory V FV]
    (M N : Action V G) : FunLike (HomSubtype V G M N) (CV M.V) (CV N.V)
    where
  coe f := f.1
  coe_injective' _ _ h := Subtype.ext (DFunLike.coe_injective h)

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