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
🔸 coverage
@[reducible, inline]
abbrev RingAut (R : Type u_1) [Mul R] [Add R] :
Type u_1

The group of ring automorphisms.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    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).

    source
    🔸 coverage
    @[implicit_reducible]
    instance RingAut.instInhabited (R : Type u_1) [Mul R] [Add R] :
    Inhabited (RingAut R)
    source
    🔸 coverage
    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
      🔸 coverage
      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
        🔸 coverage
        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
          📐 coverage
          theorem RingAut.one_eq_refl {R : Type u_1} [Mul R] [Add R] :
          1 = RingEquiv.refl R
          source
          📐 coverage
          @[simp]
          theorem RingAut.one_apply {R : Type u_1} [Mul R] [Add R] (x : R) :
          1 x = x
          source
          📐 coverage
          @[simp]
          theorem RingAut.coe_one {R : Type u_1} [Mul R] [Add R] :
          ⇑1 = id
          source
          📐 coverage
          @[simp]
          theorem RingAut.mul_apply {R : Type u_1} [Mul R] [Add R] (f g : R ≃+* R) (x : R) :
          (f * g) x = f (g x)
          source
          📐 coverage
          @[simp]
          theorem RingAut.inv_apply {R : Type u_1} [Mul R] [Add R] (f : R ≃+* R) (x : R) :
          f⁻¹ x = f.symm x
          source
          📐 coverage
          @[simp]
          theorem RingAut.coe_pow {R : Type u_1} [Mul R] [Add R] (f : R ≃+* R) (n : ℕ) :
          ⇑(f ^ n) = (⇑f)^[n]