instPreservesMonomorphismsActionFintypeCatAutFunctorFunctorToAction

English

The action functor functorToAction F reflects isomorphisms.

Русский

Действие functorToAction F отражает изоморфизмы.

LaTeX

$$$CategoryTheory.PreGaloisCategory.functorToAction F \\text{ ReflectsIsomorphisms}$$$

Lean4

instance : PreservesMonomorphisms (functorToAction F) :=
  have : PreservesMonomorphisms (functorToAction F ⋙ forget₂ _ FintypeCat) :=
    inferInstanceAs <| PreservesMonomorphisms F
  preservesMonomorphisms_of_preserves_of_reflects (functorToAction F) (forget₂ _ FintypeCat)

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