Module

RingActionOrderReflection.lean

Nyll.SchemeTheory.RingTheory.Ramification.RingActionOrderReflection

1 declaration indexed from sourceView source ↗

Module documentation

Reflection of automorphism powers along injections

Proves that a power of a ring automorphism is the identity whenever the same power of a compatible extension is the identity and the coefficient map is injective.

Imports1

Mathlib.Algebra.Ring.Aut

Imported by2

theorem

ringEquiv_pow_eq_one_of_extension

L22 ↗

SchemeTheory.ringEquiv_pow_eq_one_of_extension

Documentation

The order of an actual coefficient automorphism is reflected by its injective field extension; the iterated coefficient square is proved.

Source context 2 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace SchemeTheory
universe u v

Lean source · statement

theorem ringEquiv_pow_eq_one_of_extension
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    (f : R →+* S) (hf : Function.Injective f)
    (σ : R ≃+* R) (ρ : S ≃+* S)
    (hcoeff : ρ.toRingHom.comp f = f.comp σ.toRingHom)
    (n : ℕ) (hρ : ρ ^ n = 1) : σ ^ n = 1

Module documentation

Reflection of automorphism powers along injections

Declarations

ringEquiv_pow_eq_one_of_extension