NYLL
Module

CommAlgIdealInertiaConjugate.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgIdealInertiaConjugate
2 declarations indexed from sourceView source ↗

Module documentation

Conjugation in intrinsic ideal inertia

Defines conjugation of intrinsic ideal inertia by a stabilizer element and identifies its underlying coefficient algebra automorphism.

Imports6
Imported by5

Declarations

def

commAlgIdealInertiaConjugate

L27 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealInertiaConjugate
Documentation

The intrinsic ideal inertia conjugate, retaining the existing coefficient-automorphism action inside its native owner.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
def commAlgIdealInertiaConjugate
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B.carrier)
    (d : (commAlgIdealDecompositionGroup A B Q).carrier)
    (σ : (commAlgIdealInertiaGroup A B Q).carrier) :
    (commAlgIdealInertiaGroup A B Q).carrier
theorem

commAlgIdealInertiaConjugate_value

L36 ↗
EtaleFundamentalGroups.Inertia.commAlgIdealInertiaConjugate_value
Documentation

The native intrinsic conjugate retains the literal coefficient algebra-automorphism expression.

Source context 2 commands

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

namespace EtaleFundamentalGroups.Inertia
universe u v
Lean source · statement
theorem commAlgIdealInertiaConjugate_value
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B.carrier)
    (d : (commAlgIdealDecompositionGroup A B Q).carrier)
    (σ : (commAlgIdealInertiaGroup A B Q).carrier) :
    (commAlgIdealInertiaConjugate A B Q d σ).val = d.val * σ.val * d.val⁻¹

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