Structures · Category theory
CategoryTheory.PreGaloisCategory.IsNaturalSMul
We say G acts naturally on the fibers of F if for every f : X ⟶ Y, the G-actions
on F.obj X and F.obj Y are compatible with F.map f.
- Shape
- 2 explicit arguments · adds naturality
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- CategoryTheory.PreGaloisCategory.toAut
- CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality
- CategoryTheory.PreGaloisCategory.action_ext_of_isGalois
- CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois
- CategoryTheory.PreGaloisCategory.toAut_hom_app_apply
- CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family
- CategoryTheory.PreGaloisCategory.toAut_continuous
- CategoryTheory.PreGaloisCategory.toAut_injective_of_non_trivial
- CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitive
- CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective
- CategoryTheory.PreGaloisCategory.toAut.congr_simp
Ancestors0
No ancestors.