Contravariant pushforwards of concrete group actions
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Victor Blanchi.
Created on 2022-07-09.
Last modified on 2025-10-17.
module group-theory.contravariant-pushforward-concrete-group-actions where
Imports
open import foundation.universe-levels open import group-theory.concrete-groups open import group-theory.homomorphisms-concrete-groups
Definition
module _ {l1 l2 : Level} (G : Concrete-Group l1) (H : Concrete-Group l2) (f : hom-Concrete-Group G H) where {- contravariant-pushforward-action-Concrete-Group : {l : Level} → action-Concrete-Group l G → action-Concrete-Group {!!} H contravariant-pushforward-action-Concrete-Group X y = {!!} -- The following should be constructed as a set hom-action-Concrete-Group G X ( subst-action-Concrete-Group G H f (λ y → shape-Concrete-Group H = y)) -}
Recent changes
- 2025-10-17. Fredrik Bakke. Prefer infix
=
overId
(#1517). - 2023-05-22. Fredrik Bakke, Victor Blanchi, Egbert Rijke and Jonathan Prieto-Cubides. Pre-commit stuff (#627).
- 2023-03-14. Fredrik Bakke. Remove all unused imports (#502).
- 2023-03-10. Fredrik Bakke. Additions to
fix-import
(#497). - 2023-03-09. Jonathan Prieto-Cubides. Add hooks (#495).