Topological subcategories of Action V G
#
For a concrete category V
, where the forgetful functor factors via TopCat
,
and a monoid G
, equipped with a topological space instance,
we define the full subcategory ContAction V G
of all objects of Action V G
where the induced action is continuous.
We also define a category DiscreteContAction V G
as the full subcategory of ContAction V G
,
where the underlying topological space is discrete.
Finally we define inclusion functors into Action V G
and TopCat
in terms
of HasForget₂
instances.
Equations
Equations
- One or more equations did not get rendered due to their size.
For HasForget₂ V TopCat
a predicate on an X : Action V G
saying that the induced action on
the underlying topological space is continuous.
Equations
- X.IsContinuous = ContinuousSMul G ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)
Instances For
For HasForget₂ V TopCat
, this is the full subcategory of Action V G
where the induced
action is continuous.
Instances For
Equations
- ContAction.instHasForget₂ V G = CategoryTheory.HasForget₂.trans (ContAction V G) (Action V G) V
Equations
Equations
- ContAction.instCoeAction V G = { coe := fun (X : ContAction V G) => X.obj }
A predicate on an X : ContAction V G
saying that the topology on the underlying type of X
is discrete.
Equations
- X.IsDiscrete = DiscreteTopology ↑((CategoryTheory.forget₂ (ContAction V G) TopCat).obj X)
Instances For
The "restriction" functor along a monoid homomorphism f : G →* H
,
taking actions of H
to actions of G
. This is the analogue of
Action.res
in the continuous setting.
Equations
Instances For
Restricting scalars along a composition is naturally isomorphic to restricting scalars twice.
Equations
- ContAction.resComp V f h = CategoryTheory.NatIso.ofComponents (fun (x : ContAction V K) => CategoryTheory.Iso.refl ((ContAction.res V (h.comp f)).obj x)) ⋯
Instances For
If f = f'
, restriction of scalars along f
and f'
is the same.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restriction of scalars along a topological monoid isomorphism induces an equivalence of categories.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The subcategory of ContAction V G
where the topology is discrete.
Equations
Instances For
Equations
Continuous version of Functor.mapAction
.
Equations
Instances For
Continuous version of Functor.mapActionComp
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Continuous version of Functor.mapActionCongr
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Continuous version of Equivalence.mapAction
.
Equations
- One or more equations did not get rendered due to their size.