Theorems · Definition · Lie groups

TopRep.ofHom

{k : Type u} →
  {G : Type v} →
    {X Y : Type w} →
      [inst : TopologicalSpace k] →
        [inst_1 : Ring k] →
          [inst_2 : Monoid G] →
            [inst_3 : AddCommGroup X] →
              [inst_4 : Module k X] →
                [inst_5 : TopologicalSpace X] →
                  [inst_6 : IsTopologicalAddGroup X] →
                    [inst_7 : ContinuousSMul k X] →
                      [inst_8 : AddCommGroup Y] →
                        [inst_9 : Module k Y] →
                          [inst_10 : TopologicalSpace Y] →
                            [inst_11 : IsTopologicalAddGroup Y] →
                              [inst_12 : ContinuousSMul k Y] →
                                {ρ : ContRepresentation k G X} →
                                  {σ : ContRepresentation k G Y} → ContIntertwiningMap ρ σ → (TopRep.of ρ ⟶ TopRep.of σ)

Typecheck an IntertwiningMap as a morphism in TopRep.

Defined in

Mathlib.RepresentationTheory.Continuous.TopRep

Cited by

19 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceRingMonoidAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMulAddCommGroupModuleTopologicalSpaceIsTopologicalAddGroupContinuousSMul