Documentation

Mathlib.Algebra.Group.TypeTags.Hom

Transport algebra morphisms between additive and multiplicative types. #

source
def AddMonoidHom.toMultiplicative {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] :
(α →+ β) ≃ (Multiplicative α →* Multiplicative β)

Reinterpret α →+ β as Multiplicative α →* Multiplicative β.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem AddMonoidHom.toMultiplicative_symm_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] (f : Multiplicative α →* Multiplicative β) (a : α) :
    (toMultiplicative.symm f) a = Multiplicative.toAdd (f (Multiplicative.ofAdd a))
    source
    @[simp]
    theorem AddMonoidHom.toMultiplicative_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (a : Multiplicative α) :
    (toMultiplicative f) a = Multiplicative.ofAdd (f (Multiplicative.toAdd a))
    source
    @[simp]
    theorem AddMonoidHom.coe_toMultiplicative {α : Type u} {β : Type v} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) :
    ⇑(toMultiplicative f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Multiplicative.toAdd
    source
    def MonoidHom.toAdditive {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] :
    (α →* β) ≃ (Additive α →+ Additive β)

    Reinterpret α →* β as Additive α →+ Additive β.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MonoidHom.toAdditive_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] (f : α →* β) (a : Additive α) :
      (toAdditive f) a = Additive.ofMul (f (Additive.toMul a))
      source
      @[simp]
      theorem MonoidHom.toAdditive_symm_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] (f : Additive α →+ Additive β) (a : α) :
      (toAdditive.symm f) a = Additive.toMul (f (Additive.ofMul a))
      source
      @[simp]
      theorem MonoidHom.coe_toMultiplicative {α : Type u} {β : Type v} [MulOneClass α] [MulOneClass β] (f : α →* β) :
      ⇑(toAdditive f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Additive.toMul
      source
      def AddMonoidHom.toMultiplicative' {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] :
      (Additive α →+ β) ≃ (α →* Multiplicative β)

      Reinterpret Additive α →+ β as α →* Multiplicative β.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem AddMonoidHom.toMultiplicative'_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) (a : α) :
        (toMultiplicative' f) a = Multiplicative.ofAdd (f (Additive.ofMul a))
        source
        @[simp]
        theorem AddMonoidHom.toMultiplicative'_symm_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) (a : Additive α) :
        (toMultiplicative'.symm f) a = Multiplicative.toAdd (f (Additive.toMul a))
        source
        @[simp]
        theorem AddMonoidHom.coe_toMultiplicative' {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f : Additive α →+ β) :
        ⇑(toMultiplicative' f) = ⇑Multiplicative.ofAdd ∘ ⇑f ∘ ⇑Additive.ofMul
        source
        def MonoidHom.toAdditive' {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] :
        (α →* Multiplicative β) ≃ (Additive α →+ β)

        Reinterpret α →* Multiplicative β as Additive α →+ β.

        Equations
        Instances For
          source
          @[simp]
          theorem MonoidHom.toAdditive'_symm_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (a✝ : Additive α →+ β) (a : α) :
          (toAdditive'.symm a✝) a = Multiplicative.ofAdd (a✝ (Additive.ofMul a))
          source
          @[simp]
          theorem MonoidHom.toAdditive'_apply_apply {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (a✝ : α →* Multiplicative β) (a : Additive α) :
          (toAdditive' a✝) a = Multiplicative.toAdd (a✝ (Additive.toMul a))
          source
          @[simp]
          theorem MonoidHom.coe_toAdditive' {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f : α →* Multiplicative β) :
          ⇑(toAdditive' f) = ⇑Multiplicative.toAdd ∘ ⇑f ∘ ⇑Additive.toMul
          source
          def AddMonoidHom.toMultiplicative'' {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] :
          (α →+ Additive β) ≃ (Multiplicative α →* β)

          Reinterpret α →+ Additive β as Multiplicative α →* β.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem AddMonoidHom.toMultiplicative''_symm_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) (a : α) :
            (toMultiplicative''.symm f) a = Additive.ofMul (f (Multiplicative.ofAdd a))
            source
            @[simp]
            theorem AddMonoidHom.toMultiplicative''_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) (a : Multiplicative α) :
            (toMultiplicative'' f) a = Additive.toMul (f (Multiplicative.toAdd a))
            source
            @[simp]
            theorem AddMonoidHom.coe_toMultiplicative'' {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f : α →+ Additive β) :
            ⇑(toMultiplicative'' f) = ⇑Additive.toMul ∘ ⇑f ∘ ⇑Multiplicative.toAdd
            source
            def MonoidHom.toAdditive'' {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] :
            (Multiplicative α →* β) ≃ (α →+ Additive β)

            Reinterpret Multiplicative α →* β as α →+ Additive β.

            Equations
            Instances For
              source
              @[simp]
              theorem MonoidHom.toAdditive''_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (a✝ : Multiplicative α →* β) (a : α) :
              (toAdditive'' a✝) a = Additive.ofMul (a✝ (Multiplicative.ofAdd a))
              source
              @[simp]
              theorem MonoidHom.toAdditive''_symm_apply_apply {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (a✝ : α →+ Additive β) (a : Multiplicative α) :
              (toAdditive''.symm a✝) a = Additive.toMul (a✝ (Multiplicative.toAdd a))
              source
              @[simp]
              theorem MonoidHom.coe_toAdditive'' {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f : Multiplicative α →* β) :
              ⇑(toAdditive'' f) = ⇑Additive.ofMul ∘ ⇑f ∘ ⇑Multiplicative.ofAdd
              source
              theorem Multiplicative.monoidHom_ext {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] (f g : Multiplicative α →* β) (h : MonoidHom.toAdditive'' f = MonoidHom.toAdditive'' g) :
              f = g

              This ext lemma moves the type tag to the codomain, since most ext lemmas act on the domain.

              WARNING: This has the potential to send ext into a loop if someone locally adds the inverse ext lemma proving equality in α →+ Additive β from equality in Multiplicative α →* β.

              source
              theorem Multiplicative.monoidHom_ext_iff {α : Type u} {β : Type v} [AddZeroClass α] [MulOneClass β] {f g : Multiplicative α →* β} :
              f = g ↔ MonoidHom.toAdditive'' f = MonoidHom.toAdditive'' g
              source
              theorem Additive.addMonoidHom_ext {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] (f g : Additive α →+ β) (h : AddMonoidHom.toMultiplicative' f = AddMonoidHom.toMultiplicative' g) :
              f = g

              This ext lemma moves the type tag to the codomain, since most ext lemmas act on the domain.

              WARNING: This has the potential to send ext into a loop if someone locally adds the inverse ext lemma proving equality in α →* Multiplicative β from equality in Additive α →+ β.

              source
              theorem Additive.addMonoidHom_ext_iff {α : Type u} {β : Type v} [MulOneClass α] [AddZeroClass β] {f g : Additive α →+ β} :
              f = g ↔ AddMonoidHom.toMultiplicative' f = AddMonoidHom.toMultiplicative' g