Module

CommAlgInertiaConjugateRingHom.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgInertiaConjugateRingHom

1 declaration indexed from sourceView source ↗

Module documentation

The coefficient ring map of intrinsic inertia conjugation

Intrinsic algebra-automorphism operations are closed in this native owner. The output uses only composition of the actual coefficient ring maps.

Imports4

Imported by2

theorem

commAlgIdealInertiaConjugate_ringHom

L25 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealInertiaConjugate_ringHom

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v

Lean source · statement

theorem commAlgIdealInertiaConjugate_ringHom
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B.carrier)
    (d : (commAlgIdealDecompositionGroup A B Q).carrier)
    (σ : (commAlgIdealInertiaGroup A B Q).carrier) :
    commAlgIdealInertiaRingHom A B Q (commAlgIdealInertiaConjugate A B Q d σ) =
      (commAlgAutomorphismRingHom A B d.val).comp
        ((commAlgIdealInertiaRingHom A B Q σ).comp
          (commAlgAutomorphismRingHom A B (d⁻¹).val))

Module documentation

The coefficient ring map of intrinsic inertia conjugation

Declarations

commAlgIdealInertiaConjugate_ringHom