NYLL
Module

NativeIdealInertiaConjugate.lean

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

Module documentation

Conjugation of original ideal inertia

Constructs conjugation by an ideal stabilizer element on the original ideal inertia group and records its underlying group expression.

Imports2
  • Mathlib.Algebra.Group.Subgroup.Map
  • Mathlib.RingTheory.Ideal.Pointwise
Imported by5

Declarations

def

nativeIdealInertiaConjugate

L24 ↗
EtaleFundamentalGroups.Inertia.nativeIdealInertiaConjugate
Documentation

Conjugation by an actual ideal stabilizer preserves the original ideal inertia.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v
Lean source · statement
def nativeIdealInertiaConjugate
    (B : Type u) [CommRing B] (G : Type v) [Group G] [MulSemiringAction G B]
    (Q : Ideal B) (d : MulAction.stabilizer G Q) (σ : Q.inertia G) : Q.inertia G
theorem

nativeIdealInertiaConjugate_value

L34 ↗
EtaleFundamentalGroups.Inertia.nativeIdealInertiaConjugate_value
Documentation

The conjugation owner retains the literal original group expression.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v
Lean source · statement
theorem nativeIdealInertiaConjugate_value
    (B : Type u) [CommRing B] (G : Type v) [Group G] [MulSemiringAction G B]
    (Q : Ideal B) (d : MulAction.stabilizer G Q) (σ : Q.inertia G) :
    (nativeIdealInertiaConjugate B G 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.