Theorems · Definition · category theory
Action.FintypeCat.ofMulAction
(G : Type u_1) → (H : FintypeCat) → [inst : Monoid G] → [MulAction G H.obj] → Action FintypeCat G
Bundles a finite type H with a multiplicative action of G as an Action.
- Defined in
- Mathlib.CategoryTheory.Action.Concrete
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Monoidstatement and proof · cited by 3,887
- Finitestatement · cited by 3,029
- CategoryTheory.ObjectProperty.FullSubcategory.objstatement and proof · cited by 1,316
- MulActionstatement and proof · cited by 1,294
- MulEquiv.symmproof · cited by 482
- MonoidHom.compproof · cited by 469
- FintypeCatstatement and proof · cited by 217
- Actionstatement · cited by 206
- MulEquiv.toMonoidHomproof · cited by 126
- CategoryTheory.InducedCategory.endEquivproof · cited by 5
- TypeCat.endEquivproof · cited by 3
- MulAction.toEndHomproof · cited by 1
Cited by17
Results whose statement or proof uses this declaration.
- CategoryTheory.PreGaloisCategory.functorToActionproof · cited by 8
- Action.FintypeCat.quotientToQuotientOfLEstatement · cited by 2
- Action.FintypeCat.toEndHomstatement · cited by 2
- CategoryTheory.FintypeCat.Action.pretransitive_of_isConnectedproof · cited by 1
- CategoryTheory.PreGaloisCategory.exists_lift_of_quotient_openSubgroupstatement and proof · cited by 1
- CategoryTheory.PreGaloisCategory.fiberIsoQuotientStabilizerstatement · cited by 1
- CategoryTheory.FintypeCat.Action.isConnected_of_transitivestatement and proof · cited by 1
- Action.FintypeCat.quotientToEndHomstatement · cited by 1
- CategoryTheory.FintypeCat.isoQuotientStabilizerOfIsConnectedstatement · cited by 1
- CategoryTheory.PreGaloisCategory.has_decomp_quotientsstatement and proof · cited by 1
- CategoryTheory.PreGaloisCategory.exists_lift_of_continuousproof · cited by 0
- Action.FintypeCat.quotientToQuotientOfLE.congr_simpstatement · cited by 0