ModuleRestrictionFullyFaithful.lean
Nyll.EtaleFundamentalGroups.ContinuousActions.RestrictionFullyFaithful
2 declarations indexed from sourceView source ↗ Module documentation
Fullness of restriction for continuous actions
Restriction of continuous actions along a surjective continuous monoid homomorphism is full.
Imports1
- Mathlib.CategoryTheory.Action.Continuous
Imported by3
Declarations
CategoryTheory.ContAction.resFaithful
DocumentationRestriction of continuous actions is faithful.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u v w
open CategoryTheory
namespace CategoryTheory.ContAction
variable (V : Type u) [Category.{w} V]
variable {FV : V → V → Type w} {CV : V → Type v}
variable [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)]
variable [ConcreteCategory V FV] [HasForget₂ V TopCat]
variable {G H : Type*} [Monoid G] [TopologicalSpace G]
variable [Monoid H] [TopologicalSpace H]
CategoryTheory.ContAction.full_res
DocumentationRestriction of continuous actions along a surjective continuous monoid homomorphism is full.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u v w
open CategoryTheory
namespace CategoryTheory.ContAction
variable (V : Type u) [Category.{w} V]
variable {FV : V → V → Type w} {CV : V → Type v}
variable [∀ X Y, FunLike (FV X Y) (CV X) (CV Y)]
variable [ConcreteCategory V FV] [HasForget₂ V TopCat]
variable {G H : Type*} [Monoid G] [TopologicalSpace G]
variable [Monoid H] [TopologicalSpace H]