Smooth discrete topological representations

An object X : TopRep R G carries one continuous operator X.ρ g per group element, and nothing in that data forces the assignment g ↦ X.ρ g to be continuous in the group variable. So an object whose underlying module happens to be discrete can still have non-open point stabilizers, and there is no dictionary between all of TopRep R G and the discrete G-modules of Mathlib's unbundled classes.

This file cuts out the subcategory where such a dictionary does exist. TauCeti.IsSmoothDiscrete says that the underlying module is discrete and that every set {g | X.ρ g x = x} is open, which for a discrete module over a topological group is exactly continuity of the action; TauCeti.ofDiscreteModule turns a discrete G-module into an object of TopRep R G; and on the discrete G-modules whose G-action is continuous — not on all of them — the two translations are shown to be mutually inverse, both on objects and on morphisms.

The construction TauCeti.ofDiscreteModule itself is available for every discrete G-module, since a discrete module makes each operator continuous whatever the action does in the group variable. It is only its smoothness that needs ContinuousSMul G M, and that hypothesis cannot be dropped: TauCeti.not_isSmoothDiscrete_ofDiscreteModule_units_zmod exhibits a discrete module with a discontinuous action whose object is discrete but not smooth. So the source side of the dictionary is the discrete G-modules with continuous G-action, and the image of the unrestricted construction is larger than the smooth discrete subcategory.

The general smoothness facts for trivial topological representations also live here, since they provide the basic examples of smooth discrete objects used by coefficient constructions.

Main definitions

• TauCeti.ofDiscreteModule: a discrete G-module as an object of TopRep R G.
• TauCeti.IsSmoothDiscrete: the objects of TopRep R G whose underlying module is discrete and whose point stabilizers are open.
• TopRep.distribMulAction: the G-action on the underlying module of an object of TopRep R G, read off from its operators.
• TauCeti.ofDiscreteModuleMap: a G-equivariant R-linear map of discrete modules as a morphism of TopRep R G.
• TauCeti.ofDiscreteModuleIso: a G-equivariant R-linear equivalence of discrete modules as an isomorphism of TopRep R G.
• TauCeti.ofDiscreteModulePair: a compatible pair (φ : H →* G, f : M →ₗ[R] N) as the morphism TopRep.res φ (ofDiscreteModule R G M) ⟶ ofDiscreteModule R H N that ContinuousCohomology.map consumes.
• TauCeti.SmoothDiscreteTopRep, TauCeti.smoothDiscreteι: the smooth discrete objects as a full subcategory of TopRep R G, and its inclusion functor.
• TauCeti.DiscreteRep: the discrete G-modules with continuous G-action as a category, the source side of the dictionary in bundled form; its morphisms are Mathlib's Representation.IntertwiningMaps.
• TauCeti.toSmoothDiscrete, TauCeti.ofSmoothDiscrete: the two translations as functors.
• TauCeti.smoothDiscreteResFunctor: restriction to a subgroup as a functor between the smooth discrete subcategories; TauCeti.smoothDiscreteResTopRep is its object map as a transparent abbreviation.

Main results

• TauCeti.isSmoothDiscrete_iff_continuousSMul: for a topological group, smoothness of a discrete object is continuity of the action map G × X.V → X.V.
• TauCeti.isSmoothDiscrete_iff_discreteTopology_and_isContinuous: the predicate is Mathlib's Action.IsContinuous together with discreteness, read on Action (TopModuleCat R) G through TopRep.toActionTopModFunc, so the subcategory below is Mathlib's DiscreteContAction carried across TopRep.TopRepEquivActionTop rather than a second notion.
• TauCeti.ofDiscreteModule_isSmoothDiscrete: a discrete G-module with continuous G-action lands in the subcategory.
• TauCeti.ofDiscreteModule_eq_self: conversely, a discrete object is the image of its own underlying module.
• TauCeti.ofDiscreteModuleHomAddEquiv: morphisms between objects in the image are exactly the G-equivariant R-linear maps.
• TauCeti.ofDiscreteModulePair_eq_of_hom_apply: the compatible pair is the only morphism with its underlying map, which is how statements phrased with it are specialised; TauCeti.ofDiscreteModulePair_heq_of_hom_apply is its heterogeneous form, for group homomorphisms that agree only propositionally.
• TauCeti.res_ofDiscreteModule: the dictionary commutes with restriction to a subgroup, on the nose.
• TauCeti.isSmoothDiscrete_of_ρ_apply_eq_self: a discrete object with trivial action is smooth discrete.
• TauCeti.IsSmoothDiscrete.res: smoothness is inherited by restriction along a continuous homomorphism.
• TauCeti.isSmoothDiscrete_trivial: a trivial representation on a discrete module is smooth discrete.
• TauCeti.discreteRepEquivSmoothTopRep: for a topological group G, the two translations are an equivalence of categories between TauCeti.DiscreteRep R G and TauCeti.SmoothDiscreteTopRep R G.
• TauCeti.not_isSmoothDiscrete_ofDiscreteModule_units_zmod: a discrete object that is not smooth, so the subcategory is proper and the continuity hypothesis above is needed.

Implementation notes

• The coefficient ring is an arbitrary topological ring R, and the group is only a Monoid wherever the proofs allow. The equivalence of categories is stated for a topological group: over a topological monoid, open point stabilizers need not make the action continuous.
• TauCeti.ofDiscreteModule takes R and G explicitly, since neither is determined by the module M alone.
• TauCeti.DiscreteRep carries a field continuousSMulRing for ContinuousSMul R V, without which the underlying module is not an object of TopModuleCat R and TauCeti.ofDiscreteModule does not apply.
• Morphisms of TauCeti.DiscreteRep are Mathlib's Representation.IntertwiningMaps rather than a new structure, continuity being automatic on discrete modules.

The carrier TopRep and its functoriality are Mathlib's, and are consumed rather than restated.

The action on the underlying module

TopRep is Mathlib's type, so its namespace is Mathlib's: the derived action and its companions sit in the root TopRep namespace, not under TauCeti, which is what makes X.distribMulAction elaborate as dot notation.

@[instance_reducible]

def TopRep.distribMulAction {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) : DistribMulAction G ↑X

The G-action on the underlying module of an object of TopRep R G, read off from its operators. This is the object half of the translation back to Mathlib's unbundled classes. It is not a global instance; files that need it declare it a local instance, as this one does below. Its behaviour is TopRep.distribMulAction_smul; the body is @[expose]d only because the round trip of the dictionary below (TauCeti.discreteRepEquivSmoothTopRep) returns an object carrying this very instance, and identifying it with the one it started from is a definitional step.

Equations

• X.distribMulAction = DistribMulAction.compHom (↑X) (ContRepresentation.toRepresentation R G (↑X) X.ρ)

@[simp]

theorem TopRep.distribMulAction_smul {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (g : G) (x : ↑X) : g • x = (X.ρ g) x

In the derived action, g • x is ρ(g) x.

theorem TopRep.smulCommClass {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) : SMulCommClass G R ↑X

The derived G-action commutes with the scalars, because every operator is R-linear.

theorem TopRep.toActionTopModFunc_smul {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] (X : TopRep R G) (g : G) (x : ↑((CategoryTheory.forget₂ (Action (TopModuleCat R) G) TopCat).obj (toActionTopModFunc.obj X))) : g • x = (X.ρ g) x

The action that Mathlib's Action.IsContinuous reads on TopRep.toActionTopModFunc.obj X is the derived action TopRep.distribMulAction on X.V. Both the underlying space and the action compute away: TopRep.toActionTopModFunc.obj X has carrier TopModuleCat.of R X.V, forgotten to X.V, and its operator at g is X.ρ g transported along TopModuleCat.endRingEquiv and back, so g • x unfolds to X.ρ g x. This is the identification the two smoothness criteria below are bridged by.

theorem TopRep.isContinuous_toActionTopModFunc_iff {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Monoid G] [TopologicalSpace G] (X : TopRep R G) : (toActionTopModFunc.obj X).IsContinuous ↔ ContinuousSMul G ↑X

Mathlib's continuity condition on the object of Action (TopModuleCat R) G named by TopRep.toActionTopModFunc is continuity of the derived action on X.V. Both sides are ContinuousSMul G of the same action on the same space, by TopRep.toActionTopModFunc_smul; Action.IsContinuous is by definition the left-hand ContinuousSMul.

theorem TopRep.coe_stabilizer {R : Type u_1} [Ring R] [TopologicalSpace R] {G : Type u_2} [Group G] (X : TopRep R G) (x : ↑X) : ↑(MulAction.stabilizer G x) = {g : G | (X.ρ g) x = x}

The point stabilizers of the derived action, as sets, are the sets {g | X.ρ g x = x} that TauCeti.IsSmoothDiscrete is phrased with. This is the bridge between Mathlib's MulAction.stabilizer, in which continuousSMul_iff_stabilizer_isOpen is stated, and that phrasing.

Discrete modules as topological representations

def TauCeti.ofDiscreteModule (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] (M : Type w) [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] : TopRep R G

A discrete G-module, in Mathlib's unbundled classes, as an object of TopRep R G. Every operator is continuous because the module is discrete, which is all this construction needs; continuity in the group variable is a separate hypothesis ContinuousSMul G M, carried by TauCeti.ofDiscreteModule_isSmoothDiscrete. So the result is a discrete object of TopRep R G for any discrete module, and a smooth discrete one as soon as that hypothesis is available; TauCeti.not_isSmoothDiscrete_ofDiscreteModule_units_zmod is a module where it is not.

This is the continuous counterpart of Rep.ofDistribMulAction. The body is @[expose]d because a consumer must see that the underlying module of the result is M itself before it can state anything about the elements of that module.

Equations

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

@[simp]

theorem TauCeti.ofDiscreteModule_V (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] (M : Type w) [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] : ↑(ofDiscreteModule R G M) = M

The underlying module of ofDiscreteModule R G M is M.

instance TauCeti.instDiscreteTopologyVOfDiscreteModule (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] (M : Type w) [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] : DiscreteTopology ↑(ofDiscreteModule R G M)

The underlying topological module of TauCeti.ofDiscreteModule is discrete. This is TauCeti.ofDiscreteModule_V read as an instance: the equality holds by definition but not at reducible transparency, so instance search cannot find the discreteness of M through the projection on its own.

@[simp]

theorem TauCeti.ofDiscreteModule_ρ_apply_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] (g : G) (m : M) : ((ofDiscreteModule R G M).ρ g) m = g • m

In ofDiscreteModule R G M, the operator of g is the given action m ↦ g • m.

Smooth discrete objects

structure TauCeti.IsSmoothDiscrete (R : Type u) [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] (X : TopRep R G) : Prop

An object of TopRep R G is smooth discrete when its underlying module is discrete and every point stabilizer {g | X.ρ g x = x} is open. For a discrete module over a topological group the second condition is exactly continuity of the action in the group variable (TauCeti.isSmoothDiscrete_iff_continuousSMul), which the data of TopRep does not supply.

• discreteTopology : DiscreteTopology ↑X

  the underlying module is discrete

• stabilizer_isOpen (x : ↑X) : IsOpen {g : G | (X.ρ g) x = x}

  every point stabilizer is open

theorem TauCeti.isSmoothDiscrete_of_ρ_apply_eq_self (R : Type u) [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] (X : TopRep R G) [DiscreteTopology ↑X] (htriv : ∀ (g : G) (x : ↑X), (X.ρ g) x = x) : IsSmoothDiscrete R X

A discrete topological representation on which every operator fixes every point is smooth discrete.

theorem TauCeti.isSmoothDiscrete_trivial (R : Type u) [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] (M : Type w) [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [ContinuousSMul R M] : IsSmoothDiscrete R (TopRep.of (ContRepresentation.trivial R G M))

A trivial representation on a discrete module is smooth discrete: every point stabilizer is the whole monoid.

theorem TauCeti.IsSmoothDiscrete.res {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {H : Type u_1} [Monoid H] [TopologicalSpace H] {φ : H →* G} (hφ : Continuous ⇑φ) {X : TopRep R G} (hX : IsSmoothDiscrete R X) : IsSmoothDiscrete R (TopRep.of (X.ρ.restrict φ))

Smoothness is inherited by restriction along a continuous homomorphism: the stabilizers of the restricted object are the preimages under φ of the stabilizers of X. The restriction is written TopRep.of (X.ρ.restrict φ) rather than TopRep.res φ X only so that G may be a monoid: Mathlib declares TopRep.res under a [Group G] section variable. Nothing is lost, because TopRep.res is a reducible abbreviation for exactly this object, so for a group G this lemma proves the goal IsSmoothDiscrete R (TopRep.res φ X) verbatim.

@[simp]

theorem TauCeti.ofDiscreteModule_eq_self {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] (X : TopRep R G) [DiscreteTopology ↑X] : ofDiscreteModule R G ↑X = X

A discrete object is the image of its own underlying module under the dictionary; openness of the stabilizers plays no part, and a smooth discrete object supplies the discreteness through TauCeti.IsSmoothDiscrete.discreteTopology. Read on a smooth discrete X, whose underlying module then has a continuous action by TauCeti.IsSmoothDiscrete.continuousSMul, this and TauCeti.ofDiscreteModule_isSmoothDiscrete are the object half of the equivalence between the discrete G-modules with continuous G-action and the smooth discrete objects of TopRep R G. Read on an arbitrary discrete X it says less: the image of TauCeti.ofDiscreteModule over all discrete modules is every discrete object, smooth or not (TauCeti.not_isSmoothDiscrete_ofDiscreteModule_units_zmod).

theorem TauCeti.ofDiscreteModule_isSmoothDiscrete (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] [TopologicalSpace G] (M : Type w) [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] [ContinuousSMul G M] : IsSmoothDiscrete R (ofDiscreteModule R G M)

The dictionary lands in the smooth discrete subcategory: the point stabilizer of m is the preimage of the open set {m} under the continuous map g ↦ g • m.

theorem TauCeti.isSmoothDiscrete_iff_continuousSMul {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) [DiscreteTopology ↑X] : IsSmoothDiscrete R X ↔ ContinuousSMul G ↑X

For a discrete object of TopRep R G, smoothness is continuity of the action map G × X.V → X.V.

theorem TauCeti.IsSmoothDiscrete.continuousSMul {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X : TopRep R G} (hX : IsSmoothDiscrete R X) : ContinuousSMul G ↑X

The derived action on a smooth discrete object is continuous, so the underlying module of such an object is a discrete G-module in the unbundled classes.

theorem TauCeti.isSmoothDiscrete_iff_discreteTopology_and_isContinuous {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : TopRep R G) : IsSmoothDiscrete R X ↔ DiscreteTopology ↑X ∧ (TopRep.toActionTopModFunc.obj X).IsContinuous

Smoothness is Mathlib's continuity condition on the corresponding object of Action (TopModuleCat R) G, transported along TopRep.toActionTopModFunc: the two conditions of TauCeti.IsSmoothDiscrete are exactly ContAction.IsDiscrete and Action.IsContinuous there. So the smooth discrete objects of TopRep R G are the objects TopRep.TopRepEquivActionTop carries into DiscreteContAction (TopModuleCat R) G, and this file introduces no second notion. The predicate is nonetheless stated on TopRep R G directly, because that is the carrier continuousCohomology is defined on.

The dictionary on objects and morphisms

def TauCeti.ofDiscreteModuleMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] (f : M →ₗ[R] N) (hf : ∀ (g : G) (m : M), f (g • m) = g • f m) : ofDiscreteModule R G M ⟶ ofDiscreteModule R G N

A G-equivariant R-linear map of discrete modules as a morphism of TopRep R G. Continuity is automatic, the source being discrete. The body is @[expose]d because the exposed equivalence of categories below, TauCeti.discreteRepEquivSmoothTopRep, is built from this constructor, and its definitional checks unfold it.

Equations

• TauCeti.ofDiscreteModuleMap f hf = TopRep.ofHom (let __ContinuousLinearMap := { toLinearMap := f, cont := ⋯ }; { toContinuousLinearMap := __ContinuousLinearMap, isIntertwining' := ⋯ })

@[simp]

theorem TauCeti.ofDiscreteModuleMap_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] (f : M →ₗ[R] N) (hf : ∀ (g : G) (m : M), f (g • m) = g • f m) (m : M) : (TopRep.Hom.hom (ofDiscreteModuleMap f hf)) m = f m

ofDiscreteModuleMap f hf acts on underlying modules as f.

@[simp]

theorem TauCeti.ofDiscreteModuleMap_id {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] : ofDiscreteModuleMap LinearMap.id ⋯ = CategoryTheory.CategoryStruct.id (ofDiscreteModule R G M)

The morphism half of the dictionary preserves identities: the identity linear map of a discrete module becomes the identity morphism of the object it names.

@[simp]

theorem TauCeti.ofDiscreteModuleMap_comp_ofDiscreteModuleMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] {P : Type w} [AddCommGroup P] [Module R P] [TopologicalSpace P] [DiscreteTopology P] [DistribMulAction G P] [SMulCommClass G R P] [ContinuousSMul R P] (f : M →ₗ[R] N) (hf : ∀ (g : G) (m : M), f (g • m) = g • f m) (f' : N →ₗ[R] P) (hf' : ∀ (g : G) (n : N), f' (g • n) = g • f' n) : CategoryTheory.CategoryStruct.comp (ofDiscreteModuleMap f hf) (ofDiscreteModuleMap f' hf') = ofDiscreteModuleMap (f' ∘ₗ f) ⋯

The morphism half of the dictionary preserves composition: the composite of the morphisms named by two G-equivariant R-linear maps is the morphism named by their composite.

def TauCeti.ofDiscreteModuleIso {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] (e : M ≃ₗ[R] N) (he : ∀ (g : G) (m : M), e (g • m) = g • e m) : ofDiscreteModule R G M ≅ ofDiscreteModule R G N

A G-equivariant R-linear equivalence of discrete modules as an isomorphism of TopRep R G, with ofDiscreteModuleMap of the equivalence and of its inverse as the two directions. The inverse is equivariant by MulActionHom.inverse.

Equations

• TauCeti.ofDiscreteModuleIso e he = { hom := TauCeti.ofDiscreteModuleMap (↑e) he, inv := TauCeti.ofDiscreteModuleMap ↑e.symm ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TauCeti.ofDiscreteModuleIso_hom {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] (e : M ≃ₗ[R] N) (he : ∀ (g : G) (m : M), e (g • m) = g • e m) : (ofDiscreteModuleIso e he).hom = ofDiscreteModuleMap (↑e) he

The forward direction of ofDiscreteModuleIso e he is ofDiscreteModuleMap of e.

@[simp]

theorem TauCeti.ofDiscreteModuleIso_inv_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] (e : M ≃ₗ[R] N) (he : ∀ (g : G) (m : M), e (g • m) = g • e m) (n : N) : (TopRep.Hom.hom (ofDiscreteModuleIso e he).inv) n = e.symm n

The inverse direction of ofDiscreteModuleIso e he acts on underlying modules as e.symm.

def TauCeti.ofDiscreteModuleHomAddEquiv (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] (M : Type w) [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] (N : Type w) [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] : (ofDiscreteModule R G M ⟶ ofDiscreteModule R G N) ≃+ (Representation.ofDistribMulAction R G M).IntertwiningMap (Representation.ofDistribMulAction R G N)

The additive bijection between the morphisms of TopRep R G from ofDiscreteModule R G M to ofDiscreteModule R G N and Mathlib's Representation.IntertwiningMaps of the underlying representations: a morphism between two objects in the image of the dictionary is exactly a G-equivariant R-linear map, continuity of such a map being automatic on discrete modules. On modules with continuous G-action the right-hand side is also, by definition, the type of morphisms of TauCeti.DiscreteRep R G, so this is the hom-set bijection that the equivalence TauCeti.discreteRepEquivSmoothTopRep realises; continuity in the group variable is irrelevant to the statement, so it is proved here without that hypothesis.

Equations

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

@[simp]

theorem TauCeti.ofDiscreteModuleHomAddEquiv_apply_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] (φ : ofDiscreteModule R G M ⟶ ofDiscreteModule R G N) (m : M) : ((ofDiscreteModuleHomAddEquiv R G M N) φ) m = (TopRep.Hom.hom φ) m

ofDiscreteModuleHomAddEquiv sends a morphism φ to its underlying map.

@[simp]

theorem TauCeti.ofDiscreteModuleHomAddEquiv_symm_apply_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] (f : (Representation.ofDistribMulAction R G M).IntertwiningMap (Representation.ofDistribMulAction R G N)) (m : M) : (TopRep.Hom.hom ((ofDiscreteModuleHomAddEquiv R G M N).symm f)) m = f m

The inverse of ofDiscreteModuleHomAddEquiv sends an intertwining map f to the morphism acting as f.

The dictionary on compatible pairs

def TauCeti.ofDiscreteModulePair {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] {H : Type u_1} [Monoid H] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [SMulCommClass H R N] [ContinuousSMul R N] (φ : H →* G) (f : M →ₗ[R] N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) : TopRep.res φ (ofDiscreteModule R G M) ⟶ ofDiscreteModule R H N

The canonical-side coefficient morphism of a compatible pair: a monoid homomorphism φ : H →* G together with an f : M →ₗ[R] N satisfying f (φ h • m) = h • f m becomes a morphism TopRep.res φ (ofDiscreteModule R G M) ⟶ ofDiscreteModule R H N, which is what ContinuousCohomology.map consumes. Continuity of f is automatic, the source being discrete. TauCeti.ofDiscreteModuleMap is the case φ = MonoidHom.id G, by TauCeti.ofDiscreteModulePair_id.

Equations

• TauCeti.ofDiscreteModulePair φ f hf = TopRep.ofHom (let __ContinuousLinearMap := { toLinearMap := f, cont := ⋯ }; { toContinuousLinearMap := __ContinuousLinearMap, isIntertwining' := ⋯ })

@[simp]

theorem TauCeti.ofDiscreteModulePair_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] {H : Type u_1} [Monoid H] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [SMulCommClass H R N] [ContinuousSMul R N] (φ : H →* G) (f : M →ₗ[R] N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (m : M) : (TopRep.Hom.hom (ofDiscreteModulePair φ f hf)) m = f m

The compatible pair ofDiscreteModulePair φ f hf acts on underlying modules as f.

theorem TauCeti.ofDiscreteModulePair_eq_of_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] {H : Type u_1} [Monoid H] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [SMulCommClass H R N] [ContinuousSMul R N] (φ : H →* G) (f : M →ₗ[R] N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (ψ : TopRep.res φ (ofDiscreteModule R G M) ⟶ ofDiscreteModule R H N) (hψ : ∀ (m : M), (TopRep.Hom.hom ψ) m = f m) : ofDiscreteModulePair φ f hf = ψ

The compatible pair is determined by its underlying map: any morphism TopRep.res φ (ofDiscreteModule R G M) ⟶ ofDiscreteModule R H N whose underlying function is f is the compatible pair, morphisms of TopRep being determined by their underlying functions. This is how a statement phrased with TauCeti.ofDiscreteModulePair is specialised to a morphism presented some other way — as an identity morphism, or as TauCeti.ofDiscreteModuleMap — without its body having to be unfolded at the use site.

theorem TauCeti.ofDiscreteModulePair_heq_of_hom_apply {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] {H : Type u_1} [Monoid H] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction H N] [SMulCommClass H R N] [ContinuousSMul R N] {φ ψ : H →* G} (hφ : φ = ψ) (f : M →ₗ[R] N) (hf : ∀ (h : H) (m : M), f (φ h • m) = h • f m) (g : TopRep.res ψ (ofDiscreteModule R G M) ⟶ ofDiscreteModule R H N) (hg : ∀ (m : M), (TopRep.Hom.hom g) m = f m) : ofDiscreteModulePair φ f hf ≍ g

The heterogeneous form of TauCeti.ofDiscreteModulePair_eq_of_hom_apply: a morphism TopRep.res ψ (ofDiscreteModule R G M) ⟶ ofDiscreteModule R H N whose underlying function is f is heterogeneously equal to the compatible pair along any φ = ψ. This compares compatible pairs whose group homomorphisms agree only propositionally, so that their hom-types differ.

theorem TauCeti.ofDiscreteModulePair_id {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] {N : Type w} [AddCommGroup N] [Module R N] [TopologicalSpace N] [DiscreteTopology N] [DistribMulAction G N] [SMulCommClass G R N] [ContinuousSMul R N] (f : M →ₗ[R] N) (hf : ∀ (g : G) (m : M), f (g • m) = g • f m) : ofDiscreteModulePair (MonoidHom.id G) f hf = ofDiscreteModuleMap f hf

At the identity homomorphism the compatible pair is the coefficient morphism TauCeti.ofDiscreteModuleMap; restricting an object along the identity leaves it unchanged.

theorem TauCeti.res_ofDiscreteModule {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] {M : Type w} [AddCommGroup M] [Module R M] [TopologicalSpace M] [DiscreteTopology M] [DistribMulAction G M] [SMulCommClass G R M] [ContinuousSMul R M] (S : Subgroup G) : TopRep.res S.subtype (ofDiscreteModule R G M) = ofDiscreteModule R (↥S) M

The dictionary commutes with restriction to a subgroup: restricting the canonical object of a discrete G-module along S ↪ G is the canonical object of the same module over S, on the nose rather than up to isomorphism. The two sides are definitionally equal, so a morphism into or out of one is already a morphism of the other; this lemma names the identification for rw.

The two coefficient categories

@[reducible, inline]

abbrev TauCeti.SmoothDiscreteTopRep (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] [TopologicalSpace G] : Type (max (max u v) (w + 1))

The full subcategory of TopRep R G on the smooth discrete objects. Its inclusion into TopRep R G is TauCeti.smoothDiscreteι. For a topological group G it is equivalent to TauCeti.DiscreteRep R G (TauCeti.discreteRepEquivSmoothTopRep); for a topological monoid, open point stabilizers need not make the action continuous, and TauCeti.toSmoothDiscrete need not be essentially surjective.

Equations

• TauCeti.SmoothDiscreteTopRep R G = CategoryTheory.ObjectProperty.FullSubcategory fun (X : TopRep R G) => TauCeti.IsSmoothDiscrete R X

@[reducible, inline]

abbrev TauCeti.smoothDiscreteι (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] [TopologicalSpace G] : CategoryTheory.Functor (SmoothDiscreteTopRep R G) (TopRep R G)

The inclusion of the smooth discrete objects into TopRep R G. This is how such an object reaches Mathlib's continuousCohomology n and ContinuousCohomology.map, which are defined on TopRep R G.

Equations

• TauCeti.smoothDiscreteι R G = CategoryTheory.ObjectProperty.ι fun (X : TopRep R G) => TauCeti.IsSmoothDiscrete R X

structure TauCeti.DiscreteRep (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] [TopologicalSpace G] : Type (max (max u v) (w + 1))

A discrete G-module with continuous G-action, bundled: the source side of the dictionary as a category. For a topological group G it is equivalent to TauCeti.SmoothDiscreteTopRep R G (TauCeti.discreteRepEquivSmoothTopRep). The fields are exactly the instances TauCeti.ofDiscreteModule and TauCeti.ofDiscreteModule_isSmoothDiscrete ask for.

• V : Type w

  the underlying module

• addCommGroup : AddCommGroup self.V

  the additive group structure on V

• module : Module R self.V

  the R-module structure on V

• topologicalSpace : TopologicalSpace self.V

  the topology on V

• discreteTopology : DiscreteTopology self.V

  the topology on V is discrete

• distribMulAction : DistribMulAction G self.V

  the action of G on V by additive maps

• smulCommClass : SMulCommClass G R self.V

  the action of G commutes with the scalars

• continuousSMulRing : ContinuousSMul R self.V

  scalar multiplication by R is continuous

• continuousSMul : ContinuousSMul G self.V

  the action of G is continuous

@[reducible, inline]

abbrev TauCeti.DiscreteRep.ρ {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] (X : DiscreteRep R G) : Representation R G X.V

The representation of G on the underlying module of a discrete G-module: Mathlib's Representation.ofDistribMulAction at the module's own action. This is the representation whose intertwining maps are the morphisms of TauCeti.DiscreteRep below.

Equations

• X.ρ = Representation.ofDistribMulAction R G X.V

@[instance_reducible]

instance TauCeti.instCategoryDiscreteRep {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] : CategoryTheory.Category.{w, max (max u v) (w + 1)} (DiscreteRep R G)

The discrete G-modules with continuous G-action form a category under Mathlib's Representation.IntertwiningMaps of the representations they carry, that is, under the G-equivariant R-linear maps. Continuity is automatic on discrete modules (continuous_of_discreteTopology), so nothing is carried beyond Mathlib's type. These are the morphisms of the source side, not the morphisms of TopRep R G transported along the dictionary, so TauCeti.discreteRepEquivSmoothTopRep proves the morphism dictionary rather than assuming it.

Equations

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

@[simp]

theorem TauCeti.DiscreteRep.id_toLinearMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] (X : DiscreteRep R G) : (CategoryTheory.CategoryStruct.id X).toLinearMap = LinearMap.id

Mathlib's Representation.IntertwiningMap.toLinearMap_id, read at the categorical identity: the left-hand side of Mathlib's lemma is Representation.IntertwiningMap.id X.ρ, so it does not by itself rewrite a goal phrased with 𝟙 X.

@[simp]

theorem TauCeti.DiscreteRep.comp_toLinearMap {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {X Y Z : DiscreteRep R G} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).toLinearMap = g.toLinearMap ∘ₗ f.toLinearMap

Mathlib's Representation.IntertwiningMap.comp_toLinearMap, read at the categorical composition, which reverses the order of the arguments.

theorem TauCeti.DiscreteRep.equivariant {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] {X Y : DiscreteRep R G} (f : X ⟶ Y) (g : G) (x : X.V) : f.toLinearMap (g • x) = g • f.toLinearMap x

Equivariance of a morphism of discrete G-modules, phrased with the modules' own actions rather than with the representations TauCeti.DiscreteRep.ρ that Representation.IntertwiningMap.isIntertwining is stated for.

def TauCeti.toSmoothDiscrete (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] [TopologicalSpace G] : CategoryTheory.Functor (DiscreteRep R G) (SmoothDiscreteTopRep R G)

The dictionary going in, as a functor: a discrete G-module with continuous G-action goes to the smooth discrete object it names, and an equivariant map to the morphism it names.

Equations

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

@[simp]

theorem TauCeti.toSmoothDiscrete_obj_obj (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] [TopologicalSpace G] (X : DiscreteRep R G) : ((toSmoothDiscrete R G).obj X).obj = ofDiscreteModule R G X.V

toSmoothDiscrete sends a discrete representation X to ofDiscreteModule R G X.V.

@[simp]

theorem TauCeti.toSmoothDiscrete_map_hom_hom_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Monoid G] [TopologicalSpace G] {X Y : DiscreteRep R G} (f : X ⟶ Y) (x : X.V) : (TopRep.Hom.hom ((toSmoothDiscrete R G).map f).hom) x = f.toLinearMap x

toSmoothDiscrete sends a morphism f to the morphism acting as f.

Restriction to a subgroup

@[reducible, inline]

abbrev TauCeti.smoothDiscreteResTopRep {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R G) : SmoothDiscreteTopRep R ↥U

Restriction of a bundled smooth discrete representation to a subgroup, as an object whose underlying representation is definitionally TopRep.res U.subtype A.obj. The object map of smoothDiscreteResFunctor is not exposed, so statements that must see this definitional equality (for instance the domain of coindTraceHom) use this abbreviation instead.

Equations

• TauCeti.smoothDiscreteResTopRep U A = { obj := TopRep.res U.subtype A.obj, property := ⋯ }

def TauCeti.smoothDiscreteResFunctor (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] (U : Subgroup G) : CategoryTheory.Functor (SmoothDiscreteTopRep R G) (SmoothDiscreteTopRep R ↥U)

Restriction along U → G on smooth discrete representations.

Equations

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

@[simp]

theorem TauCeti.smoothDiscreteResFunctor_obj (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] (U : Subgroup G) (A : SmoothDiscreteTopRep R G) : (smoothDiscreteResFunctor R G U).obj A = { obj := TopRep.res U.subtype A.obj, property := ⋯ }

Restriction along U → G restricts the underlying topological representation.

@[simp]

theorem TauCeti.smoothDiscreteResFunctor_map_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] (U : Subgroup G) {A B : SmoothDiscreteTopRep R G} (f : A ⟶ B) (x : ↑A.obj) : (((TopRep.Hom.hom (CategoryTheory.eqToHom ⋯)).comp (TopRep.Hom.hom ((smoothDiscreteResFunctor R G U).map f).hom)).comp (TopRep.Hom.hom (CategoryTheory.eqToHom ⋯))) x = (TopRep.Hom.hom f.hom) x

Restriction along U → G does not change the underlying map of a morphism. The object transports identify the opaque functor's objects with the restricted representations.

The equivalence of coefficient categories

instance TauCeti.instDiscreteTopologyOfSmoothDiscrete {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Monoid G] [TopologicalSpace G] (X : SmoothDiscreteTopRep R G) : DiscreteTopology ↑X.obj

The underlying module of a smooth discrete object is discrete. This is what lets the object map of TauCeti.ofSmoothDiscrete below build a TauCeti.DiscreteRep on it, and what downstream constructions on smooth discrete objects use to treat their modules as discrete.

theorem TauCeti.instContinuousSMulOfSmoothDiscrete {R : Type u} [Ring R] [TopologicalSpace R] {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : SmoothDiscreteTopRep R G) : ContinuousSMul G ↑X.obj

The derived action on a smooth discrete object is continuous.

def TauCeti.ofSmoothDiscrete (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.Functor (SmoothDiscreteTopRep R G) (DiscreteRep R G)

The dictionary coming back, as a functor: a smooth discrete object goes to its underlying module, with the action read off from its operators by TopRep.distribMulAction.

Equations

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

@[simp]

theorem TauCeti.ofSmoothDiscrete_obj_V (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : SmoothDiscreteTopRep R G) : ((ofSmoothDiscrete R G).obj X).V = ↑X.obj

ofSmoothDiscrete keeps the underlying module of a smooth discrete representation.

@[simp]

theorem TauCeti.ofSmoothDiscrete_map_toLinearMap_apply (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] {X Y : SmoothDiscreteTopRep R G} (φ : X ⟶ Y) (x : ↑X.obj) : ((ofSmoothDiscrete R G).map φ).toLinearMap x = (TopRep.Hom.hom φ.hom) x

ofSmoothDiscrete sends a morphism φ to its underlying linear map.

@[simp]

theorem TauCeti.ofSmoothDiscrete_obj_smul (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : SmoothDiscreteTopRep R G) (g : G) (x : ((ofSmoothDiscrete R G).obj X).V) : g • x = (X.obj.ρ g) x

The action carried by the module read off a smooth discrete object is the object's own action.

def TauCeti.discreteRepEquivSmoothTopRep (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : DiscreteRep R G ≌ SmoothDiscreteTopRep R G

The dictionary is an equivalence of categories between the discrete G-modules with continuous G-action and the smooth discrete objects of TopRep R G. It is the identity on underlying modules in both directions, the action being read off by TopRep.distribMulAction, so every component of the unit and of the counit is an identity morphism.

Equations

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

@[simp]

theorem TauCeti.discreteRepEquivSmoothTopRep_functor (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (discreteRepEquivSmoothTopRep R G).functor = toSmoothDiscrete R G

The functor of discreteRepEquivSmoothTopRep is toSmoothDiscrete.

@[simp]

theorem TauCeti.discreteRepEquivSmoothTopRep_inverse (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : (discreteRepEquivSmoothTopRep R G).inverse = ofSmoothDiscrete R G

The inverse functor of discreteRepEquivSmoothTopRep is ofSmoothDiscrete.

@[simp]

theorem TauCeti.discreteRepEquivSmoothTopRep_unitIso_hom_app (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : DiscreteRep R G) : (discreteRepEquivSmoothTopRep R G).unitIso.hom.app X = CategoryTheory.CategoryStruct.id X

Each component of the unit of discreteRepEquivSmoothTopRep is an identity morphism.

@[simp]

theorem TauCeti.discreteRepEquivSmoothTopRep_unitIso_inv_app (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : DiscreteRep R G) : (discreteRepEquivSmoothTopRep R G).unitIso.inv.app X = CategoryTheory.CategoryStruct.id X

Each component of the inverse of the unit of discreteRepEquivSmoothTopRep is an identity morphism.

@[simp]

theorem TauCeti.discreteRepEquivSmoothTopRep_counitIso_hom_app (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : SmoothDiscreteTopRep R G) : (discreteRepEquivSmoothTopRep R G).counitIso.hom.app X = CategoryTheory.CategoryStruct.id X

Each component of the counit of discreteRepEquivSmoothTopRep is an identity morphism.

@[simp]

theorem TauCeti.discreteRepEquivSmoothTopRep_counitIso_inv_app (R : Type u) [Ring R] [TopologicalSpace R] (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (X : SmoothDiscreteTopRep R G) : (discreteRepEquivSmoothTopRep R G).counitIso.inv.app X = CategoryTheory.CategoryStruct.id X

Each component of the inverse of the counit of discreteRepEquivSmoothTopRep is an identity morphism.

The smooth discrete subcategory is proper

@[instance_reducible]

def TauCeti.instTopologicalSpaceUnitsZModThree : TopologicalSpace (ZMod 3)ˣ

The group of the non-example below carries the indiscrete topology, whose only open sets are ∅ and the whole group.

Equations

• TauCeti.instTopologicalSpaceUnitsZModThree = ⊤

theorem TauCeti.not_isSmoothDiscrete_ofDiscreteModule_units_zmod : ¬IsSmoothDiscrete ℤ (ofDiscreteModule ℤ (ZMod 3)ˣ (ZMod 3))

An object of TopRep R G whose underlying module is discrete need not be smooth. Here the two-element group (ZMod 3)ˣ acts on the discrete module ZMod 3 by multiplication, so the stabilizer of 1 is the singleton {1}; giving the group the indiscrete topology makes that singleton non-open. This is why the dictionary above has the discrete G-modules with continuous G-action as its source, and it is what the hypothesis ContinuousSMul G M of TauCeti.ofDiscreteModule_isSmoothDiscrete rules out. Stating it needs TauCeti.ofDiscreteModule to be available without that hypothesis, which is why the hypothesis sits on the results that use it rather than on the construction.