English
The type HomSubtype(V,G; M,N) consists of V-morphisms between the underlying objects M.V and N.V that commute with the G-action for every g in G.
Русский
Тип HomSubtype(V,G; M,N) состоит из морфизмов между M.V и N.V, которые commute с воздействием G для каждого элемента g ∈ G.
LaTeX
$$HomSubtype(V,G)(M,N) = { f: FV M.V N.V // ∀ g ∈ G, f ∘ M.ρ(g) = N.ρ(g) ∘ f }$$
Lean4
/-- The type of `V`-morphisms that can be lifted back to morphisms in the category `Action`. -/
abbrev HomSubtype {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) :=
{ f : FV M.V N.V // ∀ g : G, f ∘ ConcreteCategory.hom (M.ρ g) = ConcreteCategory.hom (N.ρ g) ∘ f }
