NYLL
Module

NativeIdealInertiaInclusion.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeIdealInertiaInclusion
4 declarations indexed from sourceView source ↗

Module documentation

Ideal inertia included into its actual stabilizer

The subgroup order and pointwise ideal-action interfaces are closed here, with only a ring and its acting group. The map is the literal inclusion.

Imports4
Imported by3

Declarations

def

nativeIdealInertiaToStabilizer

L26 ↗
EtaleFundamentalGroups.Inertia.nativeIdealInertiaToStabilizer
Documentation

The standard subgroup inclusion supplied by actual inertia stability.

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 nativeIdealInertiaToStabilizer
    (B : Type u) [CommRing B] (G : Type v) [Group G] [MulSemiringAction G B]
    (Q : Ideal B) : Q.inertia G →* MulAction.stabilizer G Q
theorem

nativeIdealInertiaToStabilizer_conjugate

L32 ↗
EtaleFundamentalGroups.Inertia.nativeIdealInertiaToStabilizer_conjugate
Documentation

This literal inclusion identifies the native conjugate with stabilizer conjugation.

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 nativeIdealInertiaToStabilizer_conjugate
    (B : Type u) [CommRing B] (G : Type v) [Group G] [MulSemiringAction G B]
    (Q : Ideal B) (d : MulAction.stabilizer G Q) (σ : Q.inertia G) :
    (nativeIdealInertiaToStabilizer B G Q).toFun
        (nativeIdealInertiaConjugate B G Q d σ) =
      d * (nativeIdealInertiaToStabilizer B G Q).toFun σ * d⁻¹
theorem

nativeIdealInertiaToStabilizer_injective

L42 ↗
EtaleFundamentalGroups.Inertia.nativeIdealInertiaToStabilizer_injective
Documentation

The literal ideal-inertia inclusion is injective.

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 nativeIdealInertiaToStabilizer_injective
    (B : Type u) [CommRing B] (G : Type v) [Group G] [MulSemiringAction G B]
    (Q : Ideal B) : Function.Injective (nativeIdealInertiaToStabilizer B G Q).toFun
theorem

nativeIdealInertiaToStabilizer_range_map

L48 ↗
EtaleFundamentalGroups.Inertia.nativeIdealInertiaToStabilizer_range_map
Documentation

Its range has exactly the original inertia image in the acting group.

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 nativeIdealInertiaToStabilizer_range_map
    (B : Type u) [CommRing B] (G : Type v) [Group G] [MulSemiringAction G B]
    (Q : Ideal B) :
    (nativeIdealInertiaToStabilizer B G Q).range.map
        (MulAction.stabilizer G Q).subtype = Q.inertia G

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