Documentation

Mathlib.Algebra.Ring.Aut

Ring automorphisms #

This file defines the automorphism group structure on RingAut R := RingEquiv R R.

Implementation notes #

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

Tags #

ring aut

source
@[reducible, inline]
abbrev RingAut (R : Type u_1) [Mul R] [Add R] :
Type u_1

The group of ring automorphisms.

Equations
    Instances For
      source
      instance RingAut.instGroup (R : Type u_1) [Mul R] [Add R] :
      Group (RingAut R)

      The group operation on automorphisms of a ring is defined by fun g h => RingEquiv.trans h g. This means that multiplication agrees with composition, (g*h)(x) = g (h x).

      Equations
        source
        instance RingAut.instInhabited (R : Type u_1) [Mul R] [Add R] :
        Inhabited (RingAut R)
        Equations
          source
          def RingAut.toAddAut (R : Type u_1) [Mul R] [Add R] :
          RingAut R →* AddAut R

          Monoid homomorphism from ring automorphisms to additive automorphisms.

          Equations
            Instances For
              source
              def RingAut.toMulAut (R : Type u_1) [Mul R] [Add R] :
              RingAut R →* MulAut R

              Monoid homomorphism from ring automorphisms to multiplicative automorphisms.

              Equations
                Instances For
                  source
                  def RingAut.toPerm (R : Type u_1) [Mul R] [Add R] :
                  RingAut R →* Equiv.Perm R

                  Monoid homomorphism from ring automorphisms to permutations.

                  Equations
                    Instances For