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] : CategoryTheory.HasForget₂ (Action V G) TopCat

Equations

• Action.instHasForget₂HomSubtypeVTopCatContinuousMapCarrier V G = CategoryTheory.HasForget₂.trans (Action V G) V TopCat

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

• One or more equations did not get rendered due to their size.

@[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) : Prop

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)

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

• ContAction V G = CategoryTheory.ObjectProperty.FullSubcategory Action.IsContinuous

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

• ContAction.instHasForget₂HomSubtypeObjActionIsContinuousV V G = CategoryTheory.HasForget₂.trans (ContAction V G) (Action V G) V

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] : CategoryTheory.HasForget₂ (ContAction V G) TopCat

Equations

• ContAction.instHasForget₂HomSubtypeObjActionIsContinuousVTopCatContinuousMapCarrier V G = CategoryTheory.HasForget₂.trans (ContAction V G) (Action V G) TopCat

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

• ContAction.instCoeAction V G = { coe := fun (X : ContAction V G) => X.obj }

@[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) : Prop

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)

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

• ContAction.res V f = CategoryTheory.ObjectProperty.lift Action.IsContinuous ((CategoryTheory.ObjectProperty.ι Action.IsContinuous).comp (Action.res V ↑f)) ⋯

@[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✝) : (res V f).map f✝ = CategoryTheory.ObjectProperty.homMk ((Action.res V ↑f).map f✝.hom)

@[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) : ((res V f).obj X).obj = (Action.res V ↑f).obj X.obj

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) : res V (h.comp f) ≅ (res V h).comp (res V f)

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)) ⋯

@[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') : res V f ≅ res V f'

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.

@[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) : ContAction V H ≌ ContAction V G

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.

@[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) : (resEquiv V f).functor = res V ↑f

@[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) : (resEquiv V f).inverse = res V ↑f.symm

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

• DiscreteContAction V G = CategoryTheory.ObjectProperty.FullSubcategory ContAction.IsDiscrete

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] : CategoryTheory.Category.{v_1, max (max u_4 u_1) v_1} (DiscreteContAction V G)

Equations

• DiscreteContAction.instCategory V G = CategoryTheory.ObjectProperty.FullSubcategory.category ContAction.IsDiscrete

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

• DiscreteContAction.instConcreteCategoryHomSubtypeObjActionIsContinuousContActionIsDiscreteV V G = CategoryTheory.FullSubcategory.concreteCategory ContAction.IsDiscrete

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

• DiscreteContAction.instHasForget₂HomSubtypeObjActionIsContinuousContActionIsDiscreteV V G = CategoryTheory.FullSubcategory.hasForget₂ ContAction.IsDiscrete

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] : CategoryTheory.HasForget₂ (DiscreteContAction V G) TopCat

Equations

• One or more equations did not get rendered due to their size.

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

• CategoryTheory.Functor.mapContAction G F H = CategoryTheory.ObjectProperty.lift Action.IsContinuous ((CategoryTheory.ObjectProperty.ι Action.IsContinuous).comp (F.mapAction G)) H

@[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✝) : (mapContAction G F H).map f = ObjectProperty.homMk ((F.mapAction G).map f.hom)

@[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) : ((mapContAction G F H).obj X).obj = (F.mapAction G).obj X.obj

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) : mapContAction G (F.comp F') ⋯ ≅ (mapContAction G F H).comp (mapContAction G F' H')

Continuous version of Functor.mapActionComp.

Equations

• One or more equations did not get rendered due to their size.

@[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) : mapContAction G F H ≅ mapContAction G F' H'

Continuous version of Functor.mapActionCongr.

Equations

• One or more equations did not get rendered due to their size.

@[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) : ContAction V G ≌ ContAction W G

Continuous version of Equivalence.mapAction.

Equations

• One or more equations did not get rendered due to their size.

@[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) : (mapContAction G E H₁ H₂).inverse = Functor.mapContAction G E.inverse H₂

@[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) : (mapContAction G E H₁ H₂).functor = Functor.mapContAction G E.functor H₁