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 Algebra/Ring/Equiv.lean
so that GroupTheory.Perm
is free to use
equivalences (and other files that use them) before the group structure is defined.
Tags #
RingAut
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
Equations
- RingAut.instInhabited R = { default := 1 }
Monoid homomorphism from ring automorphisms to additive automorphisms.
Equations
- RingAut.toAddAut R = { toFun := RingEquiv.toAddEquiv, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Monoid homomorphism from ring automorphisms to multiplicative automorphisms.
Equations
- RingAut.toMulAut R = { toFun := RingEquiv.toMulEquiv, map_one' := ⋯, map_mul' := ⋯ }
Instances For
Monoid homomorphism from ring automorphisms to permutations.
Equations
- RingAut.toPerm R = { toFun := RingEquiv.toEquiv, map_one' := ⋯, map_mul' := ⋯ }
Instances For
The tautological action by the group of automorphism of a ring R
on R
.
Equations
- RingAut.applyMulSemiringAction = MulSemiringAction.mk ⋯ ⋯
Each element of the group defines a ring automorphism.
This is a stronger version of DistribMulAction.toAddAut
and
MulDistribMulAction.toMulAut
.
Equations
- MulSemiringAction.toRingAut G R = { toFun := MulSemiringAction.toRingEquiv G R, map_one' := ⋯, map_mul' := ⋯ }