NYLL
Module

ConjugateRingAction.lean

Nyll.SchemeTheory.RingTheory.Ramification.ConjugateRingAction
2 declarations indexed from sourceView source ↗

Module documentation

Conjugation of ring automorphisms

Proves the commuting square for conjugating a ring automorphism through a ring equivalence. It also transports a compatible ambient coefficient square to the conjugated automorphism.

Imports1
  • Mathlib.Algebra.Ring.Equiv
Imported by2

Declarations

theorem

ringEquiv_conjugate_commutes

L22 ↗
SchemeTheory.ringEquiv_conjugate_commutes
Documentation

Conjugating an actual automorphism through a ring equivalence gives the actual commuting action square.

Source context 2 commands

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

namespace SchemeTheory
universe u v w
Lean source · statement
theorem ringEquiv_conjugate_commutes
    {R : Type u} {S : Type v} [CommRing R] [CommRing S]
    (e : R ≃+* S) (σ : R ≃+* R) :
    e.toRingHom.comp σ.toRingHom =
      (e.symm.trans (σ.trans e)).toRingHom.comp e.toRingHom
theorem

ringEquiv_conjugate_field_square

L34 ↗
SchemeTheory.ringEquiv_conjugate_field_square
Documentation

The original field coefficient square passes to the actual conjugated ring automorphism.

Source context 2 commands

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

namespace SchemeTheory
universe u v w
Lean source · statement
theorem ringEquiv_conjugate_field_square
    {R : Type u} {S : Type v} {F : Type w}
    [CommRing R] [CommRing S] [CommRing F]
    (e : R ≃+* S) (σ : R ≃+* R) (i : S →+* F) (ρ : F →+* F)
    (hfield : (i.comp e.toRingHom).comp σ.toRingHom =
      ρ.comp (i.comp e.toRingHom)) :
    i.comp (e.symm.trans (σ.trans e)).toRingHom = ρ.comp i

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.