imageComplementIncl — Mathlib

English

Given a morphism f: X → Y in the category of finite G-sets, the complement of the image of f carries a natural G-action induced from Y.

Русский

Пусть f: X → Y — морфизм между конечными G-множествами; дополнение образа f на Y получает естественное действие G, индуцированное действием Y.

LaTeX

$$$\\text{imageComplement } G f \\text{ is a } G\\text{-set with } (\\mathrm{ρ}g)(y) = Y.\\rho(g) y$ for y in the complement of Im(f.hom).$$

Lean4

/-- The inclusion from the complement of the image of `f : X ⟶ Y` into `Y`. -/
noncomputable def imageComplementIncl {X Y : Action FintypeCat G} (f : X ⟶ Y) : Action.imageComplement G f ⟶ Y
    where
  hom := FintypeCat.imageComplementIncl f.hom
  comm _ := rfl

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