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

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

The group of ring automorphisms.

Instances For
    source
    instance RingAut.instGroupRingAut (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).

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

    Monoid homomorphism from ring automorphisms to additive automorphisms.

    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.

      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.

        Instances For
          source
          instance RingAut.applyMulSemiringAction {R : Type u_2} [Semiring R] :
          MulSemiringAction (RingAut R) R

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

          source
          @[simp]
          theorem RingAut.smul_def {R : Type u_2} [Semiring R] (f : RingAut R) (r : R) :
          f • r = ↑f r
          source
          instance RingAut.apply_faithfulSMul {R : Type u_2} [Semiring R] :
          FaithfulSMul (RingAut R) R
          source
          @[simp]
          theorem MulSemiringAction.toRingAut_apply (G : Type u_1) (R : Type u_2) [Group G] [Semiring R] [MulSemiringAction G R] (x : G) :
          ↑(MulSemiringAction.toRingAut G R) x = MulSemiringAction.toRingEquiv G R x
          source
          def MulSemiringAction.toRingAut (G : Type u_1) (R : Type u_2) [Group G] [Semiring R] [MulSemiringAction G R] :
          G →* RingAut R

          Each element of the group defines a ring automorphism.

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

          Instances For