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.

  • toFun : AB
  • map_zero' : self.toFun 0 = 0
  • map_add' : ∀ (x y : A), self.toFun (x + y) = self.toFun x + self.toFun y
  • continuous_toFun : Continuous self.toFun

    Proof of continuity of the Hom.

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.

    • toFun : AB
    • map_one' : self.toFun 1 = 1
    • map_mul' : ∀ (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
    • continuous_toFun : Continuous self.toFun

      Proof of continuity of the Hom.

    Instances For

      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.

      • 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.

      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] [FunLike F A B] extends MonoidHomClass :

        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.

        • 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.

        Instances
          Equations
          • =
          Equations
          theorem ContinuousAddMonoidHom.funLike.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 : ContinuousAddMonoidHom A B) => f.toFun) f = (fun (f : ContinuousAddMonoidHom A B) => f.toFun) g) :
          f = g
          Equations
          • ContinuousMonoidHom.funLike = { coe := fun (f : ContinuousMonoidHom A B) => f.toFun, coe_injective' := }
          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

          Reinterpret a ContinuousAddMonoidHom as a ContinuousMap.

          Equations
          Instances For

            Reinterpret a ContinuousMonoidHom as a ContinuousMap.

            Equations
            Instances For
              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

              Construct a ContinuousAddMonoidHom from a Continuous AddMonoidHom.

              Equations
              Instances For
                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.

                Equations
                Instances For
                  theorem ContinuousAddMonoidHom.comp.proof_1 {A : Type u_1} {B : Type u_3} {C : Type u_2} [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 : A) => f.toAddMonoidHom x)

                  Composition of two continuous homomorphisms.

                  Equations
                  Instances For
                    @[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.

                    Equations
                    Instances For

                      Product of two continuous homomorphisms on the same space.

                      Equations
                      Instances For
                        theorem ContinuousAddMonoidHom.sum.proof_1 {A : Type u_1} {B : Type u_3} {C : Type u_2} [AddMonoid A] [AddMonoid B] [AddMonoid C] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace C] (f : ContinuousAddMonoidHom A B) (g : ContinuousAddMonoidHom A C) :
                        Continuous fun (x : A) => (f.toFun x, g.toAddMonoidHom x)
                        @[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)
                        @[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)

                        Product of two continuous homomorphisms on the same space.

                        Equations
                        Instances For
                          theorem ContinuousAddMonoidHom.sum_map.proof_1 {A : Type u_1} {B : Type u_2} {C : Type u_4} {D : Type u_3} [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 (p : A × B) => (f.toFun p.1, (g.toAddMonoidHom).1 p.2)

                          Product of two continuous homomorphisms on different spaces.

                          Equations
                          Instances For
                            @[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.1, g.toAddMonoidHom i.2)
                            @[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.1, g.toMonoidHom i.2)

                            Product of two continuous homomorphisms on different spaces.

                            Equations
                            Instances For

                              The trivial continuous homomorphism.

                              Equations
                              Instances For
                                theorem ContinuousAddMonoidHom.zero.proof_1 (A : Type u_1) (B : Type u_2) [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                Continuous fun (x : A) => 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.

                                Equations
                                Instances For

                                  The identity continuous homomorphism.

                                  Equations
                                  Instances For
                                    @[simp]

                                    The identity continuous homomorphism.

                                    Equations
                                    Instances For

                                      The continuous homomorphism given by projection onto the first factor.

                                      Equations
                                      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.1
                                        @[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.1

                                        The continuous homomorphism given by projection onto the first factor.

                                        Equations
                                        Instances For

                                          The continuous homomorphism given by projection onto the second factor.

                                          Equations
                                          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.2
                                            @[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.2

                                            The continuous homomorphism given by projection onto the second factor.

                                            Equations
                                            Instances For

                                              The continuous homomorphism given by inclusion of the first factor.

                                              Equations
                                              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.

                                                Equations
                                                Instances For

                                                  The continuous homomorphism given by inclusion of the second factor.

                                                  Equations
                                                  Instances For
                                                    @[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)
                                                    @[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)

                                                    The continuous homomorphism given by inclusion of the second factor.

                                                    Equations
                                                    Instances For

                                                      The continuous homomorphism given by the diagonal embedding.

                                                      Equations
                                                      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]

                                                        The continuous homomorphism given by the diagonal embedding.

                                                        Equations
                                                        Instances For

                                                          The continuous homomorphism given by swapping components.

                                                          Equations
                                                          Instances For
                                                            @[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)
                                                            @[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)

                                                            The continuous homomorphism given by swapping components.

                                                            Equations
                                                            Instances For

                                                              The continuous homomorphism given by addition.

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

                                                                The continuous homomorphism given by multiplication.

                                                                Equations
                                                                Instances For

                                                                  The continuous homomorphism given by negation.

                                                                  Equations
                                                                  Instances For

                                                                    The continuous homomorphism given by inversion.

                                                                    Equations
                                                                    Instances For
                                                                      @[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.

                                                                      Equations
                                                                      Instances For
                                                                        Equations
                                                                        • ContinuousAddMonoidHom.instAddCommGroupContinuousAddMonoidHomToAddMonoidToSubNegAddMonoidToAddGroup = AddCommGroup.mk
                                                                        Equations
                                                                        • ContinuousMonoidHom.instCommGroupContinuousMonoidHomToMonoidToDivInvMonoidToGroup = CommGroup.mk
                                                                        Equations
                                                                        • ContinuousAddMonoidHom.instTopologicalSpaceContinuousAddMonoidHom = TopologicalSpace.induced ContinuousAddMonoidHom.toContinuousMap ContinuousMap.compactOpen
                                                                        Equations
                                                                        • ContinuousMonoidHom.instTopologicalSpaceContinuousMonoidHom = TopologicalSpace.induced ContinuousMonoidHom.toContinuousMap ContinuousMap.compactOpen
                                                                        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
                                                                        theorem ContinuousAddMonoidHom.range_toContinuousMap (A : Type u_2) (B : Type u_3) [AddMonoid A] [AddMonoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                        Set.range ContinuousAddMonoidHom.toContinuousMap = {f : C(A, B) | f 0 = 0 ∀ (x y : A), f (x + y) = f x + f y}
                                                                        theorem ContinuousMonoidHom.range_toContinuousMap (A : Type u_2) (B : Type u_3) [Monoid A] [Monoid B] [TopologicalSpace A] [TopologicalSpace B] :
                                                                        Set.range ContinuousMonoidHom.toContinuousMap = {f : C(A, B) | f 1 = 1 ∀ (x y : A), f (x * y) = f x * f y}
                                                                        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 ContinuousMonoidHom.continuous_of_continuous_uncurry {B : Type u_3} {C : Type u_4} [Monoid B] [Monoid C] [TopologicalSpace B] [TopologicalSpace C] {A : Type u_7} [TopologicalSpace A] (f : AContinuousMonoidHom B C) (h : Continuous (Function.uncurry fun (x : A) (y : B) => (f x) y)) :

                                                                        ContinuousAddMonoidHom _ f is a functor.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          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) :
                                                                          { toFun := fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f, map_zero' := }.toFun (_g + _h) = { toFun := fun (g : ContinuousAddMonoidHom B E) => ContinuousAddMonoidHom.comp g f, map_zero' := }.toFun (_g + _h)

                                                                          ContinuousMonoidHom _ f is a functor.

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

                                                                            ContinuousAddMonoidHom f _ is a functor.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              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) :
                                                                              { toFun := fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g, map_zero' := }.toFun (g + h) = { toFun := fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g, map_zero' := }.toFun g + { toFun := fun (g : ContinuousAddMonoidHom A B) => ContinuousAddMonoidHom.comp f g, map_zero' := }.toFun h

                                                                              ContinuousMonoidHom f _ is a functor.

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