Algebraic representations with the discrete topology

discreteTopRepFunctor equips an algebraic representation with the discrete topology, without changing its module, action, or morphisms, so it is fully faithful. Over a discrete group its values are smooth. Restricting these objects along continuous maps to discrete quotients supplies smooth coefficient objects for continuous cohomology.

The construction retains Mathlib's Rep and TopRep carriers; it only supplies the topology and continuity proofs. Ring coefficients are required by Mathlib's TopRep.

def TauCeti.discreteTopRep (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] (A : Rep R G) : TopRep R G

An algebraic representation with the discrete topology on its underlying module. The body is exposed so the pointwise action equation can use elements of A.V directly.

@[simp]

theorem TauCeti.discreteTopRep_V (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] (A : Rep R G) : ↑(discreteTopRep R G A) = ↑A

Equipping a representation with the discrete topology preserves its underlying module.

@[simp]

theorem TauCeti.discreteTopRep_ρ_apply (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] (A : Rep R G) (g : G) (a : ↑A) : ((discreteTopRep R G A).ρ g) a = (A.ρ g) a

The action of discreteTopRep is the original algebraic action.

instance TauCeti.instDiscreteTopologyVDiscreteTopRep (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] (A : Rep R G) : DiscreteTopology ↑(discreteTopRep R G A)

Discrete topology is part of the output of discreteTopRep.

def TauCeti.discreteTopRepFunctor (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] : CategoryTheory.Functor (Rep R G) (TopRep R G)

Equip every algebraic representation and intertwining map with the discrete topology. The body is exposed so the pointwise morphism equation can use the original algebraic carriers.

instance TauCeti.instAdditiveRepTopRepDiscreteTopRepFunctor (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] : (discreteTopRepFunctor R G).Additive

Equipping intertwining maps with continuity proofs preserves addition.

@[simp]

theorem TauCeti.discreteTopRepFunctor_obj (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] (A : Rep R G) : (discreteTopRepFunctor R G).obj A = discreteTopRep R G A

The functor sends an object to its discrete topological representation.

@[simp]

theorem TauCeti.discreteTopRepFunctor_map_apply (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] {A B : Rep R G} (f : A ⟶ B) (a : ↑A) : (TopRep.Hom.hom ((discreteTopRepFunctor R G).map f)) a = (Rep.Hom.hom f) a

The functor leaves the underlying intertwining map unchanged.

instance TauCeti.instFaithfulRepTopRepDiscreteTopRepFunctor (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] : (discreteTopRepFunctor R G).Faithful

Equipping representations with the discrete topology is faithful: it leaves the underlying linear maps unchanged.

instance TauCeti.instFullRepTopRepDiscreteTopRepFunctor (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] : (discreteTopRepFunctor R G).Full

Equipping representations with the discrete topology is full: every intertwining map between discrete modules is continuous.

theorem TauCeti.isSmoothDiscrete_discreteTopRep (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (G : Type v) [Monoid G] [TopologicalSpace G] [DiscreteTopology G] (A : Rep R G) : IsSmoothDiscrete R (discreteTopRep R G A)

A representation of a discrete monoid on a discrete module is smooth.

theorem TauCeti.exists_discreteTopRep_res_iso (R : Type u) [Ring R] [TopologicalSpace R] [DiscreteTopology R] (H : Type v) [Group H] (X : TopRep R H) [DiscreteTopology ↑X] (V : Subgroup H) [V.Normal] (hV : ∀ g ∈ V, ∀ (x : ↑X), (X.ρ g) x = x) : ∃ (A : Rep R (H ⧸ V)), Nonempty (TopRep.res (QuotientGroup.mk' V) (discreteTopRep R (H ⧸ V) A) ≅ X)

A discrete topological representation on which a normal subgroup acts trivially is the inflation of an algebraic representation of the quotient, with its discrete topology.