Theorems · Definition · Lie groups

TopRep.Hom.toTopModuleCatHom

{k : Type u} →
  {G : Type v} →
    [inst : TopologicalSpace k] →
      [inst_1 : Ring k] →
        [inst_2 : Monoid G] → {A B : TopRep k G} → A.Hom B → (TopModuleCat.of k ↑A ⟶ TopModuleCat.of k ↑B)

The morphism of topological modules underlying a morphism in TopRep k G.

Defined in: Mathlib.RepresentationTheory.Continuous.TopRep
Cited by: 0 results in Mathlib
Foundations: Depth 99 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: TopologicalSpace Ring Monoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites12

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement · cited by 32,603
TopologicalSpacestatement and proof · cited by 24,529
Ringstatement and proof · cited by 7,463
Monoidstatement and proof · cited by 3,887
TopRepstatement and proof · cited by 54
TopModuleCatstatement · cited by 45
TopRep.Vstatement · cited by 36
TopRep.Hom.homproof · cited by 33
ContIntertwiningMap.toContinuousLinearMapproof · cited by 28
TopModuleCat.ofstatement · cited by 4
TopModuleCat.ofHomproof · cited by 4
TopRep.Homstatement and proof · cited by 3

Cited by1

Results whose statement or proof uses this declaration.

TopRep.toActionTopModFuncproof · cited by 0