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.

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

Tags #

RingAut

@[reducible]
def RingAut (R : Type u_1) [Mul R] [Add R] :
Type u_1

The group of ring automorphisms.

Equations
Instances For
    instance RingAut.instGroupRingAut (R : Type u_1) [Mul R] [Add 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
    instance RingAut.instInhabitedRingAut (R : Type u_1) [Mul R] [Add R] :
    Equations
    def RingAut.toAddAut (R : Type u_1) [Mul R] [Add R] :

    Monoid homomorphism from ring automorphisms to additive automorphisms.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def RingAut.toMulAut (R : Type u_1) [Mul R] [Add R] :

      Monoid homomorphism from ring automorphisms to multiplicative automorphisms.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        def RingAut.toPerm (R : Type u_1) [Mul R] [Add R] :

        Monoid homomorphism from ring automorphisms to permutations.

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

          The tautological action by the group of automorphism of a ring R on R.

          Equations
          @[simp]
          theorem RingAut.smul_def {R : Type u_2} [Semiring R] (f : RingAut R) (r : R) :
          f r = f r
          Equations

          Each element of the group defines a ring automorphism.

          This is a stronger version of DistribMulAction.toAddAut and MulDistribMulAction.toMulAut.

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