Documentation

Mathlib.Topology.Algebra.ContinuousMonoidHom

Continuous Monoid Homs #

This file defines the space of continuous homomorphisms between two topological groups.

Main definitions #

structure ContinuousAddMonoidHom (A : Type u_7) (B : Type u_8) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] extends AddMonoidHom :
Type (max u_7 u_8)

The type of continuous additive monoid homomorphisms from A to B.

Instances For
    structure ContinuousMonoidHom (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] extends MonoidHom :
    Type (max u_2 u_3)

    The type of continuous monoid homomorphisms from A to B.

    When possible, instead of parametrizing results over (f : ContinuousMonoidHom A B), you should parametrize over (F : Type*) [ContinuousMonoidHomClass F A B] (f : F).

    When you extend this structure, make sure to extend ContinuousAddMonoidHomClass.

    Instances For
      class ContinuousAddMonoidHomClass (F : Type u_1) (A : outParam (Type u_7)) (B : outParam (Type u_8)) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] extends AddMonoidHomClass :
      Type (max (max u_1 u_7) u_8)
      • coe : FAB
      • coe_injective' : Function.Injective FunLike.coe
      • map_add : ∀ (f : F) (x y : A), f (x + y) = f x + f y
      • map_zero : ∀ (f : F), f 0 = 0
      • map_continuous : ∀ (f : F), Continuous f

        Proof of the continuity of the map.

      ContinuousAddMonoidHomClass F A B states that F is a type of continuous additive monoid homomorphisms.

      You should also extend this typeclass when you extend ContinuousAddMonoidHom.

      Instances
        class ContinuousMonoidHomClass (F : Type u_1) (A : outParam (Type u_7)) (B : outParam (Type u_8)) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] extends MonoidHomClass :
        Type (max (max u_1 u_7) u_8)
        • coe : FAB
        • coe_injective' : Function.Injective FunLike.coe
        • map_mul : ∀ (f : F) (x y : A), f (x * y) = f x * f y
        • map_one : ∀ (f : F), f 1 = 1
        • map_continuous : ∀ (f : F), Continuous f

          Proof of the continuity of the map.

        ContinuousMonoidHomClass F A B states that F is a type of continuous additive monoid homomorphisms.

        You should also extend this typeclass when you extend ContinuousMonoidHom.

        Instances
          theorem ContinuousAddMonoidHom.ContinuousMonoidHom.ContinuousAddMonoidHomClass.proof_1 {A : Type u_2} {B : Type u_1} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A B) (h : (fun f => f.toFun) f = (fun f => f.toFun) g) :
          f = g
          theorem ContinuousAddMonoidHom.ContinuousMonoidHom.ContinuousAddMonoidHomClass.proof_2 {A : Type u_2} {B : Type u_1} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousAddMonoidHom A B) (x : A) (y : A) :
          ZeroHom.toFun (f.toAddMonoidHom) (x + y) = ZeroHom.toFun (f.toAddMonoidHom) x + ZeroHom.toFun (f.toAddMonoidHom) y

          Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun.

          Helper instance for when there's too many metavariables to apply FunLike.hasCoeToFun directly.

          theorem ContinuousAddMonoidHom.ext {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] {f : ContinuousAddMonoidHom A B} {g : ContinuousAddMonoidHom A B} (h : ∀ (x : A), f x = g x) :
          f = g
          theorem ContinuousMonoidHom.ext {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] {f : ContinuousMonoidHom A B} {g : ContinuousMonoidHom A B} (h : ∀ (x : A), f x = g x) :
          f = g
          theorem ContinuousAddMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
          Function.Injective ContinuousAddMonoidHom.toContinuousMap
          theorem ContinuousMonoidHom.toContinuousMap_injective {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
          Function.Injective ContinuousMonoidHom.toContinuousMap
          theorem ContinuousAddMonoidHom.mk'.proof_1 {A : Type u_2} {B : Type u_1} [AddMonoid A] [AddMonoid B] (f : A →+ B) (x : A) (y : A) :
          ZeroHom.toFun (f) (x + y) = ZeroHom.toFun (f) x + ZeroHom.toFun (f) y
          def ContinuousMonoidHom.mk' {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : A →* B) (hf : Continuous f) :

          Construct a ContinuousMonoidHom from a Continuous MonoidHom.

          Instances For

            Composition of two continuous homomorphisms.

            Instances For
              theorem ContinuousAddMonoidHom.comp.proof_1 {A : Type u_2} {B : Type u_3} {C : Type u_1} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousAddMonoidHom B C) (f : ContinuousAddMonoidHom A B) :
              Continuous (g.toFun fun x => f.toAddMonoidHom x)
              @[simp]
              theorem ContinuousAddMonoidHom.comp_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousAddMonoidHom B C) (f : ContinuousAddMonoidHom A B) :
              ∀ (a : A), ↑(ContinuousAddMonoidHom.comp g f) a = g.toAddMonoidHom (f.toAddMonoidHom a)
              @[simp]
              theorem ContinuousMonoidHom.comp_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (g : ContinuousMonoidHom B C) (f : ContinuousMonoidHom A B) :
              ∀ (a : A), ↑(ContinuousMonoidHom.comp g f) a = g.toMonoidHom (f.toMonoidHom a)

              Composition of two continuous homomorphisms.

              Instances For

                Product of two continuous homomorphisms on the same space.

                Instances For
                  theorem ContinuousAddMonoidHom.sum.proof_1 {A : Type u_3} {B : Type u_2} {C : Type u_1} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A C) :
                  Continuous fun x => (ZeroHom.toFun (f.toAddMonoidHom) x, g.toAddMonoidHom x)
                  @[simp]
                  theorem ContinuousMonoidHom.prod_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [Monoid A] [Monoid B] [Monoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousMonoidHom A B) (g : ContinuousMonoidHom A C) (i : A) :
                  ↑(ContinuousMonoidHom.prod f g) i = (f.toMonoidHom i, g.toMonoidHom i)
                  @[simp]
                  theorem ContinuousAddMonoidHom.sum_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A C) (i : A) :
                  ↑(ContinuousAddMonoidHom.sum f g) i = (f.toAddMonoidHom i, g.toAddMonoidHom i)

                  Product of two continuous homomorphisms on the same space.

                  Instances For

                    Product of two continuous homomorphisms on different spaces.

                    Instances For
                      theorem ContinuousAddMonoidHom.sum_map.proof_1 {A : Type u_3} {B : Type u_4} {C : Type u_2} {D : Type u_1} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousAddMonoidHom A C) (g : ContinuousAddMonoidHom B D) :
                      Continuous fun x => (ZeroHom.toFun (f.toAddMonoidHom) x.fst, (g.toAddMonoidHom).1 x.snd)
                      @[simp]
                      theorem ContinuousMonoidHom.prod_map_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [Monoid A] [Monoid B] [Monoid C] [Monoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousMonoidHom A C) (g : ContinuousMonoidHom B D) (i : A × B) :
                      ↑(ContinuousMonoidHom.prod_map f g) i = (f.toMonoidHom i.fst, g.toMonoidHom i.snd)
                      @[simp]
                      theorem ContinuousAddMonoidHom.sum_map_toFun {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [AddMonoid A] [AddMonoid B] [AddMonoid C] [AddMonoid D] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] [TopologicalSpace D] (f : ContinuousAddMonoidHom A C) (g : ContinuousAddMonoidHom B D) (i : A × B) :
                      ↑(ContinuousAddMonoidHom.sum_map f g) i = (f.toAddMonoidHom i.fst, g.toAddMonoidHom i.snd)

                      Product of two continuous homomorphisms on different spaces.

                      Instances For

                        The trivial continuous homomorphism.

                        Instances For
                          theorem ContinuousAddMonoidHom.zero.proof_1 (A : Type u_2) (B : Type u_1) [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                          Continuous fun x => AddZeroClass.toZero.1
                          @[simp]
                          @[simp]
                          theorem ContinuousMonoidHom.one_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                          ∀ (x : A), ↑(ContinuousMonoidHom.one A B) x = 1

                          The trivial continuous homomorphism.

                          Instances For

                            The identity continuous homomorphism.

                            Instances For
                              @[simp]

                              The identity continuous homomorphism.

                              Instances For

                                The continuous homomorphism given by projection onto the first factor.

                                Instances For
                                  @[simp]
                                  theorem ContinuousMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                  ↑(ContinuousMonoidHom.fst A B) self = self.fst
                                  @[simp]
                                  theorem ContinuousAddMonoidHom.fst_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                  ↑(ContinuousAddMonoidHom.fst A B) self = self.fst

                                  The continuous homomorphism given by projection onto the first factor.

                                  Instances For

                                    The continuous homomorphism given by projection onto the second factor.

                                    Instances For
                                      @[simp]
                                      theorem ContinuousAddMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                      ↑(ContinuousAddMonoidHom.snd A B) self = self.snd
                                      @[simp]
                                      theorem ContinuousMonoidHom.snd_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (self : A × B) :
                                      ↑(ContinuousMonoidHom.snd A B) self = self.snd

                                      The continuous homomorphism given by projection onto the second factor.

                                      Instances For

                                        The continuous homomorphism given by inclusion of the first factor.

                                        Instances For
                                          @[simp]
                                          theorem ContinuousMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) :
                                          ↑(ContinuousMonoidHom.inl A B) i = ((ContinuousMonoidHom.id A).toMonoidHom i, (ContinuousMonoidHom.one A B).toMonoidHom i)
                                          @[simp]
                                          theorem ContinuousAddMonoidHom.inl_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A) :
                                          ↑(ContinuousAddMonoidHom.inl A B) i = ((ContinuousAddMonoidHom.id A).toAddMonoidHom i, (ContinuousAddMonoidHom.zero A B).toAddMonoidHom i)

                                          The continuous homomorphism given by inclusion of the first factor.

                                          Instances For

                                            The continuous homomorphism given by inclusion of the second factor.

                                            Instances For
                                              @[simp]
                                              theorem ContinuousMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) :
                                              ↑(ContinuousMonoidHom.inr A B) i = ((ContinuousMonoidHom.one B A).toMonoidHom i, (ContinuousMonoidHom.id B).toMonoidHom i)
                                              @[simp]
                                              theorem ContinuousAddMonoidHom.inr_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : B) :
                                              ↑(ContinuousAddMonoidHom.inr A B) i = ((ContinuousAddMonoidHom.zero B A).toAddMonoidHom i, (ContinuousAddMonoidHom.id B).toAddMonoidHom i)

                                              The continuous homomorphism given by inclusion of the second factor.

                                              Instances For

                                                The continuous homomorphism given by the diagonal embedding.

                                                Instances For
                                                  @[simp]
                                                  theorem ContinuousMonoidHom.diag_toFun (A : Type u_2) [Monoid A] [TopologicalSpace A] (i : A) :
                                                  ↑(ContinuousMonoidHom.diag A) i = ((ContinuousMonoidHom.id A).toMonoidHom i, (ContinuousMonoidHom.id A).toMonoidHom i)
                                                  @[simp]
                                                  theorem ContinuousAddMonoidHom.diag_toFun (A : Type u_2) [AddMonoid A] [TopologicalSpace A] (i : A) :
                                                  ↑(ContinuousAddMonoidHom.diag A) i = ((ContinuousAddMonoidHom.id A).toAddMonoidHom i, (ContinuousAddMonoidHom.id A).toAddMonoidHom i)

                                                  The continuous homomorphism given by the diagonal embedding.

                                                  Instances For

                                                    The continuous homomorphism given by swapping components.

                                                    Instances For
                                                      @[simp]
                                                      theorem ContinuousMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) :
                                                      ↑(ContinuousMonoidHom.swap A B) i = ((ContinuousMonoidHom.snd A B).toMonoidHom i, (ContinuousMonoidHom.fst A B).toMonoidHom i)
                                                      @[simp]
                                                      theorem ContinuousAddMonoidHom.swap_toFun (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (i : A × B) :
                                                      ↑(ContinuousAddMonoidHom.swap A B) i = ((ContinuousAddMonoidHom.snd A B).toAddMonoidHom i, (ContinuousAddMonoidHom.fst A B).toAddMonoidHom i)

                                                      The continuous homomorphism given by swapping components.

                                                      Instances For

                                                        The continuous homomorphism given by addition.

                                                        Instances For
                                                          @[simp]
                                                          @[simp]
                                                          theorem ContinuousMonoidHom.mul_toFun (E : Type u_6) [CommGroup E] [TopologicalSpace E] [TopologicalGroup E] :
                                                          ∀ (a : E × E), ↑(ContinuousMonoidHom.mul E) a = a.fst * a.snd

                                                          The continuous homomorphism given by multiplication.

                                                          Instances For

                                                            The continuous homomorphism given by negation.

                                                            Instances For

                                                              The continuous homomorphism given by inversion.

                                                              Instances For

                                                                Coproduct of two continuous homomorphisms to the same space.

                                                                Instances For
                                                                  @[simp]
                                                                  @[simp]
                                                                  theorem ContinuousMonoidHom.coprod_toFun {A : Type u_2} {B : Type u_3} {E : Type u_6} [Monoid A] [Monoid B] [CommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalGroup E] (f : ContinuousMonoidHom A E) (g : ContinuousMonoidHom B E) :
                                                                  ∀ (a : A × B), ↑(ContinuousMonoidHom.coprod f g) a = (ContinuousMonoidHom.mul E).toMonoidHom ((ContinuousMonoidHom.prod_map f g).toMonoidHom a)

                                                                  Coproduct of two continuous homomorphisms to the same space.

                                                                  Instances For
                                                                    theorem ContinuousAddMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                    Inducing ContinuousAddMonoidHom.toContinuousMap
                                                                    theorem ContinuousMonoidHom.inducing_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                    Inducing ContinuousMonoidHom.toContinuousMap
                                                                    theorem ContinuousAddMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                    Embedding ContinuousAddMonoidHom.toContinuousMap
                                                                    theorem ContinuousMonoidHom.embedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                    Embedding ContinuousMonoidHom.toContinuousMap
                                                                    abbrev ContinuousAddMonoidHom.closedEmbedding_toContinuousMap.match_1 (A : Type u_1) (B : Type u_2) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousAddMonoidHom A B) (x : A) (y : A) (U : Set B) (V : Set B) (W : Set B) (motive : ContinuousAddMonoidHom.toContinuousMap f {f | f x U} {f | f y V} {f | f (x + y) W}Prop) :
                                                                    (x : ContinuousAddMonoidHom.toContinuousMap f {f | f x U} {f | f y V} {f | f (x + y) W}) → ((hfU : ContinuousAddMonoidHom.toContinuousMap f {f | f x U}) → (hfV : ContinuousAddMonoidHom.toContinuousMap f {f | f y V}) → (hfW : ContinuousAddMonoidHom.toContinuousMap f {f | f (x + y) W}) → motive (_ : ContinuousAddMonoidHom.toContinuousMap f {f | f x U} {f | f y V} ContinuousAddMonoidHom.toContinuousMap f {f | f (x + y) W})) → motive x
                                                                    Instances For
                                                                      theorem ContinuousMonoidHom.closedEmbedding_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] [ContinuousMul B] [T2Space B] :
                                                                      ClosedEmbedding ContinuousMonoidHom.toContinuousMap
                                                                      theorem ContinuousAddMonoidHom.compLeft.proof_2 {A : Type u_3} {B : Type u_2} (E : Type u_1) [AddMonoid A] [AddMonoid B] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace E] [TopologicalAddGroup E] (f : ContinuousAddMonoidHom A B) (_g : ContinuousAddMonoidHom B E) (_h : ContinuousAddMonoidHom B E) :
                                                                      ZeroHom.toFun { toFun := fun g => ContinuousAddMonoidHom.comp g f, map_zero' := (_ : (fun g => ContinuousAddMonoidHom.comp g f) 0 = (fun g => ContinuousAddMonoidHom.comp g f) 0) } (_g + _h) = ZeroHom.toFun { toFun := fun g => ContinuousAddMonoidHom.comp g f, map_zero' := (_ : (fun g => ContinuousAddMonoidHom.comp g f) 0 = (fun g => ContinuousAddMonoidHom.comp g f) 0) } (_g + _h)
                                                                      theorem ContinuousAddMonoidHom.compRight.proof_2 (A : Type u_2) {E : Type u_3} [AddMonoid A] [AddCommGroup E] [TopologicalSpace A] [TopologicalSpace E] [TopologicalAddGroup E] {B : Type u_1} [AddCommGroup B] [TopologicalSpace B] [TopologicalAddGroup B] (f : ContinuousAddMonoidHom B E) (g : ContinuousAddMonoidHom A B) (h : ContinuousAddMonoidHom A B) :
                                                                      ZeroHom.toFun { toFun := fun g => ContinuousAddMonoidHom.comp f g, map_zero' := (_ : (fun g => ContinuousAddMonoidHom.comp f g) 0 = 0) } (g + h) = ZeroHom.toFun { toFun := fun g => ContinuousAddMonoidHom.comp f g, map_zero' := (_ : (fun g => ContinuousAddMonoidHom.comp f g) 0 = 0) } g + ZeroHom.toFun { toFun := fun g => ContinuousAddMonoidHom.comp f g, map_zero' := (_ : (fun g => ContinuousAddMonoidHom.comp f g) 0 = 0) } h
                                                                      def PontryaginDual (A : Type u_2) [Monoid A] [TopologicalSpace A] :
                                                                      Type u_2

                                                                      The Pontryagin dual of A is the group of continuous homomorphism A → circle.

                                                                      Instances For

                                                                        PontryaginDual is a functor.

                                                                        Instances For
                                                                          @[simp]
                                                                          theorem PontryaginDual.map_apply {A : Type u_2} {B : Type u_3} [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] (f : ContinuousMonoidHom A B) (x : PontryaginDual B) (y : A) :
                                                                          ↑(↑(PontryaginDual.map f) x) y = x (f y)