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
    • RingAut.toAddAut R = { toOneHom := { toFun := RingEquiv.toAddEquiv, map_one' := }, map_mul' := }
    Instances For
      def RingAut.toMulAut (R : Type u_1) [Mul R] [Add R] :

      Monoid homomorphism from ring automorphisms to multiplicative automorphisms.

      Equations
      • RingAut.toMulAut R = { toOneHom := { toFun := RingEquiv.toMulEquiv, map_one' := }, map_mul' := }
      Instances For
        def RingAut.toPerm (R : Type u_1) [Mul R] [Add R] :

        Monoid homomorphism from ring automorphisms to permutations.

        Equations
        • RingAut.toPerm R = { toOneHom := { toFun := RingEquiv.toEquiv, map_one' := }, map_mul' := }
        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
          Instances For