Documentation

Mathlib.Algebra.Hom.Aut

Multiplicative and additive group automorphisms #

This file defines the automorphism group structure on AddAut R := AddEquiv R R and MulAut R := MulEquiv R R.

Implementation notes #

The definition of multiplication in the automorphism groups agrees with function composition, multiplication in Equiv.Perm, and multiplication in CategoryTheory.End, but not with CategoryTheory.comp.

This file is kept separate from Data/Equiv/MulAdd so that GroupTheory.Perm is free to use equivalences (and other files that use them) before the group structure is defined.

Tags #

MulAut, AddAut

@[reducible]
def AddAut (M : Type u_4) [Add M] :
Type u_4

The group of additive automorphisms.

Equations
Instances For
    @[reducible]
    def MulAut (M : Type u_4) [Mul M] :
    Type u_4

    The group of multiplicative automorphisms.

    Equations
    Instances For
      instance MulAut.instGroupMulAut (M : Type u_2) [Mul M] :

      The group operation on multiplicative automorphisms is defined by g h => MulEquiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

      Equations
      instance MulAut.instInhabitedMulAut (M : Type u_2) [Mul M] :
      Equations
      @[simp]
      theorem MulAut.coe_mul (M : Type u_2) [Mul M] (e₁ : MulAut M) (e₂ : MulAut M) :
      ↑(e₁ * e₂) = e₁ e₂
      @[simp]
      theorem MulAut.coe_one (M : Type u_2) [Mul M] :
      1 = id
      theorem MulAut.mul_def (M : Type u_2) [Mul M] (e₁ : MulAut M) (e₂ : MulAut M) :
      e₁ * e₂ = MulEquiv.trans e₂ e₁
      theorem MulAut.one_def (M : Type u_2) [Mul M] :
      theorem MulAut.inv_def (M : Type u_2) [Mul M] (e₁ : MulAut M) :
      @[simp]
      theorem MulAut.mul_apply (M : Type u_2) [Mul M] (e₁ : MulAut M) (e₂ : MulAut M) (m : M) :
      ↑(e₁ * e₂) m = e₁ (e₂ m)
      @[simp]
      theorem MulAut.one_apply (M : Type u_2) [Mul M] (m : M) :
      1 m = m
      @[simp]
      theorem MulAut.apply_inv_self (M : Type u_2) [Mul M] (e : MulAut M) (m : M) :
      e (e⁻¹ m) = m
      @[simp]
      theorem MulAut.inv_apply_self (M : Type u_2) [Mul M] (e : MulAut M) (m : M) :
      e⁻¹ (e m) = m
      def MulAut.toPerm (M : Type u_2) [Mul M] :

      Monoid hom from the group of multiplicative automorphisms to the group of permutations.

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

        The tautological action by MulAut M on M.

        This generalizes Function.End.applyMulAction.

        Equations
        @[simp]
        theorem MulAut.smul_def {M : Type u_4} [Monoid M] (f : MulAut M) (a : M) :
        f a = f a
        def MulAut.conj {G : Type u_3} [Group G] :

        Group conjugation, MulAut.conj g h = g * h * g⁻¹, as a monoid homomorphism mapping multiplication in G into multiplication in the automorphism group MulAut G. See also the type ConjAct G for any group G, which has a MulAction (ConjAct G) G instance where conj G acts on G by conjugation.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem MulAut.conj_apply {G : Type u_3} [Group G] (g : G) (h : G) :
          ↑(MulAut.conj g) h = g * h * g⁻¹
          @[simp]
          theorem MulAut.conj_symm_apply {G : Type u_3} [Group G] (g : G) (h : G) :
          ↑(MulEquiv.symm (MulAut.conj g)) h = g⁻¹ * h * g
          @[simp]
          theorem MulAut.conj_inv_apply {G : Type u_3} [Group G] (g : G) (h : G) :
          (MulAut.conj g)⁻¹ h = g⁻¹ * h * g
          instance AddAut.group (A : Type u_1) [Add A] :

          The group operation on additive automorphisms is defined by g h => AddEquiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

          Equations
          instance AddAut.instInhabitedAddAut (A : Type u_1) [Add A] :
          Equations
          @[simp]
          theorem AddAut.coe_mul (A : Type u_1) [Add A] (e₁ : AddAut A) (e₂ : AddAut A) :
          ↑(e₁ * e₂) = e₁ e₂
          @[simp]
          theorem AddAut.coe_one (A : Type u_1) [Add A] :
          1 = id
          theorem AddAut.mul_def (A : Type u_1) [Add A] (e₁ : AddAut A) (e₂ : AddAut A) :
          e₁ * e₂ = AddEquiv.trans e₂ e₁
          theorem AddAut.one_def (A : Type u_1) [Add A] :
          theorem AddAut.inv_def (A : Type u_1) [Add A] (e₁ : AddAut A) :
          @[simp]
          theorem AddAut.mul_apply (A : Type u_1) [Add A] (e₁ : AddAut A) (e₂ : AddAut A) (a : A) :
          ↑(e₁ * e₂) a = e₁ (e₂ a)
          @[simp]
          theorem AddAut.one_apply (A : Type u_1) [Add A] (a : A) :
          1 a = a
          @[simp]
          theorem AddAut.apply_inv_self (A : Type u_1) [Add A] (e : AddAut A) (a : A) :
          e⁻¹ (e a) = a
          @[simp]
          theorem AddAut.inv_apply_self (A : Type u_1) [Add A] (e : AddAut A) (a : A) :
          e (e⁻¹ a) = a
          def AddAut.toPerm (A : Type u_1) [Add A] :

          Monoid hom from the group of multiplicative automorphisms to the group of permutations.

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

            The tautological action by AddAut A on A.

            This generalizes Function.End.applyMulAction.

            Equations
            @[simp]
            theorem AddAut.smul_def {A : Type u_4} [AddMonoid A] (f : AddAut A) (a : A) :
            f a = f a
            def AddAut.conj {G : Type u_3} [AddGroup G] :

            Additive group conjugation, AddAut.conj g h = g + h - g, as an additive monoid homomorphism mapping addition in G into multiplication in the automorphism group AddAut G (written additively in order to define the map).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem AddAut.conj_apply {G : Type u_3} [AddGroup G] (g : G) (h : G) :
              ↑(Additive.toMul (AddAut.conj g)) h = g + h + -g
              @[simp]
              theorem AddAut.conj_symm_apply {G : Type u_3} [AddGroup G] (g : G) (h : G) :
              ↑(AddEquiv.symm (AddAut.conj g)) h = -g + h + g
              @[simp]
              theorem AddAut.conj_inv_apply {G : Type u_3} [AddGroup G] (g : G) (h : G) :
              (Additive.toMul (AddAut.conj g))⁻¹ h = -g + h + g