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.
instance
Action.instHasForget₂HomSubtypeVTopCatContinuousMapCarrier
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
:
Equations
instance
Action.instMulActionCarrierObjTopCatForget₂ContinuousMap
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
(X : Action V G)
:
MulAction G ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)
Equations
@[reducible, inline]
abbrev
Action.IsContinuous
{V : Type u_1}
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
(X : Action V G)
:
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
Instances For
theorem
Action.isContinuous_def
{V : Type u_1}
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
(X : Action V G)
:
X.IsContinuous ↔ Continuous fun (p : G × ↑((CategoryTheory.forget₂ (Action V G) TopCat).obj X)) =>
(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ V TopCat).map (X.ρ p.1))) p.2
@[reducible, inline]
abbrev
ContAction
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
Type (max (max u_1 u_4) v_1)
For HasForget₂ V TopCat, this is the full subcategory of Action V G where the induced
action is continuous.
Equations
Instances For
instance
ContAction.instHasForget₂HomSubtypeObjActionIsContinuousV
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
CategoryTheory.HasForget₂ (ContAction V G) V
Equations
instance
ContAction.instHasForget₂HomSubtypeObjActionIsContinuousVTopCatContinuousMapCarrier
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
Equations
instance
ContAction.instCoeAction
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
Coe (ContAction V G) (Action V G)
Equations
@[reducible, inline]
abbrev
ContAction.IsDiscrete
{V : Type u_1}
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
(X : ContAction V G)
:
A predicate on an X : ContAction V G saying that the topology on the underlying type of X
is discrete.
Equations
Instances For
def
ContAction.res
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f : G →ₜ* H)
:
CategoryTheory.Functor (ContAction V H) (ContAction V G)
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
@[simp]
theorem
ContAction.res_map
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f : G →ₜ* H)
{X✝ Y✝ : ContAction V H}
(f✝ : X✝ ⟶ Y✝)
:
@[simp]
theorem
ContAction.res_obj_obj
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f : G →ₜ* H)
(X : ContAction V H)
:
def
ContAction.resComp
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
{K : Type u_6}
[Monoid K]
[TopologicalSpace K]
(f : G →ₜ* H)
(h : H →ₜ* K)
:
Restricting scalars along a composition is naturally isomorphic to restricting scalars twice.
Equations
Instances For
@[simp]
theorem
ContAction.resComp_hom
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
{K : Type u_6}
[Monoid K]
[TopologicalSpace K]
(f : G →ₜ* H)
(h : H →ₜ* K)
:
(resComp V f h).hom = { app := fun (X : ContAction V K) => CategoryTheory.CategoryStruct.id ((res V (h.comp f)).obj X), naturality := ⋯ }
@[simp]
theorem
ContAction.resComp_inv
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
{K : Type u_6}
[Monoid K]
[TopologicalSpace K]
(f : G →ₜ* H)
(h : H →ₜ* K)
:
(resComp V f h).inv = { app := fun (X : ContAction V K) => CategoryTheory.CategoryStruct.id ((res V (h.comp f)).obj X), naturality := ⋯ }
def
ContAction.resCongr
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f f' : G →ₜ* H)
(h : f = f')
:
If f = f', restriction of scalars along f and f' is the same.
Equations
Instances For
@[simp]
theorem
ContAction.resCongr_hom
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f f' : G →ₜ* H)
(h : f = f')
:
(resCongr V f f' h).hom = { app := fun (X : ContAction V H) =>
CategoryTheory.ObjectProperty.homMk (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).hom,
naturality := ⋯ }
@[simp]
theorem
ContAction.resCongr_inv
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f f' : G →ₜ* H)
(h : f = f')
:
(resCongr V f f' h).inv = { app := fun (X : ContAction V H) =>
CategoryTheory.ObjectProperty.homMk (Action.mkIso (CategoryTheory.Iso.refl X.obj.V) ⋯).inv,
naturality := ⋯ }
def
ContAction.resEquiv
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f : G ≃ₜ* H)
:
Restriction of scalars along a topological monoid isomorphism induces an equivalence of categories.
Equations
Instances For
@[simp]
theorem
ContAction.resEquiv_functor
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f : G ≃ₜ* H)
:
@[simp]
theorem
ContAction.resEquiv_inverse
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
{H : Type u_5}
[Monoid H]
[TopologicalSpace H]
(f : G ≃ₜ* H)
:
def
DiscreteContAction
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
Type (max (max u_1 u_4) v_1)
The subcategory of ContAction V G where the topology is discrete.
Equations
Instances For
instance
DiscreteContAction.instCategory
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
Equations
instance
DiscreteContAction.instConcreteCategoryHomSubtypeObjActionIsContinuousContActionIsDiscreteV
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
CategoryTheory.ConcreteCategory (DiscreteContAction V G) fun (X Y : DiscreteContAction V G) =>
Action.HomSubtype V G X.obj.obj Y.obj.obj
Equations
instance
DiscreteContAction.instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteV
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
CategoryTheory.HasForget₂ (DiscreteContAction V G) (ContAction V G)
Equations
instance
DiscreteContAction.instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteVTopCatContinuousMapCarrier
(V : Type u_1)
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
(G : Type u_4)
[Monoid G]
[TopologicalSpace G]
:
Equations
instance
DiscreteContAction.instDiscreteTopologyCarrierObjTopCatForget₂ContinuousMap
{V : Type u_1}
[CategoryTheory.Category.{v_1, u_1} V]
{FV : V → V → Type u_2}
{CV : V → Type u_3}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[CategoryTheory.ConcreteCategory V FV]
[CategoryTheory.HasForget₂ V TopCat]
{G : Type u_4}
[Monoid G]
[TopologicalSpace G]
(X : DiscreteContAction V G)
:
DiscreteTopology ↑((CategoryTheory.forget₂ (DiscreteContAction V G) TopCat).obj X)
def
CategoryTheory.Functor.mapContAction
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
(F : Functor V W)
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
:
Functor (ContAction V G) (ContAction W G)
Continuous version of Functor.mapAction.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapContAction_map
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
(F : Functor V W)
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
{X✝ Y✝ : ContAction V G}
(f : X✝ ⟶ Y✝)
:
@[simp]
theorem
CategoryTheory.Functor.mapContAction_obj_obj
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
(F : Functor V W)
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
(X : ContAction V G)
:
def
CategoryTheory.Functor.mapContActionComp
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
{T : Type u_12}
[Category.{v_4, u_12} T]
{FT : T → T → Type u_13}
{CT : T → Type u_14}
[(X Y : T) → FunLike (FT X Y) (CT X) (CT Y)]
[ConcreteCategory T FT]
[HasForget₂ T TopCat]
(F : Functor V W)
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
(F' : Functor W T)
(H' : ∀ (X : ContAction W G), ((F'.mapAction G).obj X.obj).IsContinuous)
:
Continuous version of Functor.mapActionComp.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapContActionComp_hom
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
{T : Type u_12}
[Category.{v_4, u_12} T]
{FT : T → T → Type u_13}
{CT : T → Type u_14}
[(X Y : T) → FunLike (FT X Y) (CT X) (CT Y)]
[ConcreteCategory T FT]
[HasForget₂ T TopCat]
(F : Functor V W)
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
(F' : Functor W T)
(H' : ∀ (X : ContAction W G), ((F'.mapAction G).obj X.obj).IsContinuous)
:
(mapContActionComp G F H F' H').hom = { app := fun (X : ContAction V G) => CategoryStruct.id ((mapContAction G (F.comp F') ⋯).obj X), naturality := ⋯ }
@[simp]
theorem
CategoryTheory.Functor.mapContActionComp_inv
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
{T : Type u_12}
[Category.{v_4, u_12} T]
{FT : T → T → Type u_13}
{CT : T → Type u_14}
[(X Y : T) → FunLike (FT X Y) (CT X) (CT Y)]
[ConcreteCategory T FT]
[HasForget₂ T TopCat]
(F : Functor V W)
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
(F' : Functor W T)
(H' : ∀ (X : ContAction W G), ((F'.mapAction G).obj X.obj).IsContinuous)
:
(mapContActionComp G F H F' H').inv = { app := fun (X : ContAction V G) => CategoryStruct.id ((mapContAction G (F.comp F') ⋯).obj X), naturality := ⋯ }
def
CategoryTheory.Functor.mapContActionCongr
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
{F F' : Functor V W}
(e : F ≅ F')
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
(H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous)
:
Continuous version of Functor.mapActionCongr.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Functor.mapContActionCongr_hom
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
{F F' : Functor V W}
(e : F ≅ F')
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
(H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous)
:
(mapContActionCongr G e H H').hom = { app := fun (X : ContAction V G) => ObjectProperty.homMk (Action.mkIso (e.app X.obj.V) ⋯).hom, naturality := ⋯ }
@[simp]
theorem
CategoryTheory.Functor.mapContActionCongr_inv
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
{F F' : Functor V W}
(e : F ≅ F')
(H : ∀ (X : ContAction V G), ((F.mapAction G).obj X.obj).IsContinuous)
(H' : ∀ (X : ContAction V G), ((F'.mapAction G).obj X.obj).IsContinuous)
:
(mapContActionCongr G e H H').inv = { app := fun (X : ContAction V G) => ObjectProperty.homMk (Action.mkIso (e.app X.obj.V) ⋯).inv, naturality := ⋯ }
def
CategoryTheory.Equivalence.mapContAction
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
(E : V ≌ W)
(H₁ : ∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous)
(H₂ : ∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous)
:
Continuous version of Equivalence.mapAction.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Equivalence.mapContAction_inverse
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
(E : V ≌ W)
(H₁ : ∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous)
(H₂ : ∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous)
:
@[simp]
theorem
CategoryTheory.Equivalence.mapContAction_functor
{V : Type u_5}
{W : Type u_6}
[Category.{v_2, u_5} V]
{FV : V → V → Type u_7}
{CV : V → Type u_8}
[(X Y : V) → FunLike (FV X Y) (CV X) (CV Y)]
[ConcreteCategory V FV]
[HasForget₂ V TopCat]
[Category.{v_3, u_6} W]
{FW : W → W → Type u_9}
{CW : W → Type u_10}
[(X Y : W) → FunLike (FW X Y) (CW X) (CW Y)]
[ConcreteCategory W FW]
[HasForget₂ W TopCat]
(G : Type u_11)
[Monoid G]
[TopologicalSpace G]
(E : V ≌ W)
(H₁ : ∀ (X : ContAction V G), ((E.functor.mapAction G).obj X.obj).IsContinuous)
(H₂ : ∀ (X : ContAction W G), ((E.inverse.mapAction G).obj X.obj).IsContinuous)
: