English
There is a concrete category structure on Action V G whose hom-sets are given by HomSubtype with a forgetful projection to V.
Русский
Существует структура конкретной категории на Action V G: гом-отрезки задаются через HomSubtype, с проекции на V.
LaTeX
$$ConcreteCategory (Action V G) (HomSubtype V G)$$
Lean4
instance {FV : V → V → Type*} {CV : V → Type*} [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)] [ConcreteCategory V FV] :
ConcreteCategory (Action V G) (HomSubtype V G)
where
hom
f :=
⟨ConcreteCategory.hom (C := V) f.1, fun g => by
ext
simpa using CategoryTheory.congr_fun (f.2 g) _⟩
ofHom
f :=
⟨ConcreteCategory.ofHom (C := V) f, fun g =>
ConcreteCategory.ext_apply fun x => by simpa [ConcreteCategory.hom_ofHom] using congr_fun (f.2 g) x⟩
hom_ofHom _ := by dsimp; ext; simp [ConcreteCategory.hom_ofHom]
ofHom_hom _ := by ext; simp [ConcreteCategory.ofHom_hom]
id_apply := ConcreteCategory.id_apply (C := V)
comp_apply _ _ := ConcreteCategory.comp_apply (C := V) _ _
