@[reducible, inline]

abbrev CRep (R G : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] : Type (u + 1)

Equations

• CRep R G = ContAction (TopModuleCat R) G

instance instPreadditiveContActionTopModuleCat_padicRep {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] : CategoryTheory.Preadditive (ContAction (TopModuleCat R) G)

Equations

• instPreadditiveContActionTopModuleCat_padicRep = id inferInstance

instance instPreadditiveCRep {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] : CategoryTheory.Preadditive (CRep R G)

Equations

• instPreadditiveCRep = inferInstance

instance instLinearCRep {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] : CategoryTheory.Linear R (CRep R G)

Equations

• instLinearCRep = id (id inferInstance)

instance CRep.instCoeSortType {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] : CoeSort (CRep R G) (Type u)

Equations

• CRep.instCoeSortType = { coe := fun (V : CRep R G) => ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat }

def CRep.toTopModuleCat {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : TopModuleCat R

Equations

• V.toTopModuleCat = (CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V

@[reducible, inline]

abbrev CRep.toTopModuleCatMap {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] {V W : CRep R G} (f : V ⟶ W) : V.toTopModuleCat ⟶ W.toTopModuleCat

The underlying morphism in TopModuleCat induced by a morphism in CRep.

Equations

• CRep.toTopModuleCatMap f = (CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).map f

@[simp]

theorem CRep.toTopModuleCatMap_def {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] {V W : CRep R G} (f : V ⟶ W) : toTopModuleCatMap f = (CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).map f

@[reducible, inline]

abbrev CRep.toAction {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : Action (TopModuleCat R) G

Equations

• V.toAction = V.obj

@[reducible, inline]

abbrev CRep.toTop {R : Type u} [CommRing R] [TopologicalSpace R] : CategoryTheory.Functor (TopModuleCat R) TopCat

Equations

• CRep.toTop = CategoryTheory.forget₂ (TopModuleCat R) TopCat

@[reducible, inline]

abbrev CRep.act {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) (g : G) (v : ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat) : ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat

Equations

• V.act g v = (CategoryTheory.ConcreteCategory.hom (CRep.toTop.map (V.toAction.ρ g))) v

instance CRep.instAddCommGroupCarrierObjTopModuleCatForget₂ {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : AddCommGroup ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat

Equations

• V.instAddCommGroupCarrierObjTopModuleCatForget₂ = inferInstance

instance CRep.instModuleCarrierObjTopModuleCatForget₂ {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : Module R ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat

Equations

• V.instModuleCarrierObjTopModuleCatForget₂ = inferInstance

instance CRep.instTopologicalSpaceCarrierObjTopModuleCatForget₂ {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : TopologicalSpace ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat

Equations

• V.instTopologicalSpaceCarrierObjTopModuleCatForget₂ = inferInstance

instance CRep.instContinuousSMulCarrierObjTopModuleCatForget₂ {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : ContinuousSMul R ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat

theorem CRep.continuous_action {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : Continuous fun (p : G × ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat) => V.act p.1 p.2

def CRep.toRep {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : Rep R G

Equations

• V.toRep = ((CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)).mapAction G).obj V.toAction

instance CRep.instCoeRep {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] : Coe (CRep R G) (Rep R G)

Equations

• CRep.instCoeRep = { coe := CRep.toRep }

@[simp]

theorem CRep.coe_toRep {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : V.toRep = V.toRep

noncomputable def CRep.ρ {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : CRep R G) : ContinuousRep R G ↑((CategoryTheory.forget₂ (CRep R G) (TopModuleCat R)).obj V).toModuleCat

Equations

• V.ρ = ⟨V.toRep.ρ, ⋯⟩

theorem CRep.continuous_const_smul_of_continuous_action {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) (g : G) : Continuous fun (v : ↑V.V) => (V.ρ g) v

From joint continuity of the action map G × V → V, deduce pointwise continuity in V.

noncomputable def CRep.repActiontoTopModuleCatHom {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) (g : G) : TopModuleCat.of R ↑V.V ⟶ TopModuleCat.of R ↑V.V

Upgrade ((Action.ρ V) g).hom to a morphism in TopModuleCat using pointwise continuity.

Equations

• CRep.repActiontoTopModuleCatHom V hcont g = TopModuleCat.ofHom { toLinearMap := V.ρ g, cont := ⋯ }

@[simp]

theorem CRep.repActiontoTopModuleCatHom_apply {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) (g : G) (v : ↑V.V) : (CategoryTheory.ConcreteCategory.hom (repActiontoTopModuleCatHom V hcont g)) v = (V.ρ g) v

@[simp]

theorem CRep.repActiontoTopModuleCatHom_one {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) : repActiontoTopModuleCatHom V hcont 1 = CategoryTheory.CategoryStruct.id (TopModuleCat.of R ↑V.V)

The upgraded morphism sends 1 to the identity.

@[simp]

theorem CRep.repActiontoTopModuleCatHom_mul {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) (g h : G) : repActiontoTopModuleCatHom V hcont (g * h) = CategoryTheory.CategoryStruct.comp (repActiontoTopModuleCatHom V hcont h) (repActiontoTopModuleCatHom V hcont g)

The upgraded morphism respects multiplication (with the Action convention).

noncomputable def CRep.repActiontoTopModuleCatEnd {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) : G →* CategoryTheory.End (TopModuleCat.of R ↑V.V)

Assemble the upgraded morphisms into a monoid hom G →* End (TopModuleCat.of R V).

Equations

• CRep.repActiontoTopModuleCatEnd V hcont = { toFun := CRep.repActiontoTopModuleCatHom V hcont, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CRep.repActiontoTopModuleCatEnd_apply {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) (g : G) (v : ↑V.V) : (CategoryTheory.ConcreteCategory.hom (have this := (repActiontoTopModuleCatEnd V hcont) g; this)) v = (V.ρ g) v

Pointwise simp lemma for the upgraded End action.

noncomputable def CRep.ofRepAction {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) : Action (TopModuleCat R) G

The Action (TopModuleCat R) G obtained from V : Rep R G and a continuity hypothesis.

Equations

• CRep.ofRepAction V hcont = { V := TopModuleCat.of R ↑V.V, ρ := CRep.repActiontoTopModuleCatEnd V hcont }

@[simp]

theorem CRep.ofRepAction_V {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) : (ofRepAction V hcont).V = TopModuleCat.of R ↑V.V

@[simp]

theorem CRep.ofRepAction_ρ {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) (g : G) : (ofRepAction V hcont).ρ g = (repActiontoTopModuleCatEnd V hcont) g

theorem CRep.continuous_ofRepAction {R G : Type u} [CommRing R] [TopologicalSpace R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) : Continuous fun (p : G × ↑(TopModuleCat.of R ↑V.V).toModuleCat) => (CategoryTheory.ConcreteCategory.hom (toTop.map ((ofRepAction V hcont).ρ p.1))) p.2

Joint continuity of the action map for ofRepAction.

noncomputable def CRep.ofRep {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] (V : Rep R G) [TopologicalSpace ↑V.V] [ContinuousAdd ↑V.V] [ContinuousSMul R ↑V.V] (hcont : Continuous fun (p : G × ↑V.V) => (V.ρ p.1) p.2) : CRep R G

Upgrade V : Rep R G to CRep R G assuming the action map is jointly continuous.

Equations

• CRep.ofRep V hcont = { obj := CRep.ofRepAction V hcont, property := ⋯ }

@[reducible, inline]

noncomputable abbrev CRep.of {R G : Type u} [CommRing R] [TopologicalSpace R] [IsTopologicalRing R] [Group G] [TopologicalSpace G] {V : Type u} [AddCommGroup V] [Module R V] [TopologicalSpace V] [ContinuousAdd V] [ContinuousSMul R V] (ρ : ContinuousRep R G V) : CRep R G

Upgrade ρ : ContinuousRep R G V to an object of CRep R G.

This composes Rep.of with CRep.ofRep.

Equations

• CRep.of ρ = CRep.ofRep (Rep.of ↑ρ) ⋯