Module

NativeResidueAction.lean

Nyll.SchemeTheory.RingTheory.Ramification.NativeResidueAction

15 declarations indexed from sourceView source ↗

Module documentation

The actual native residue-action homomorphism

The source and target are the existing stabilizer and quotient-algebra automorphism groups. The map is exactly Ideal.Quotient.stabilizerHom. Its surjectivity is obtained from the constructed global residue equations, and its kernel mapped to the original group is the native inertia subgroup. The quotient-algebra-to-ring conversion is proved before profinite data occur.

Imports6

Nyll.SchemeTheory.RingTheory.Ramification.ProfiniteInvariantResidueLift
Mathlib.Algebra.Category.Grp.Basic
Mathlib.Algebra.Ring.Equiv
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Pointwise
Mathlib.RingTheory.Ideal.Quotient.Basic

Imported by9

def

nativeResidueStabilizer

L33 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizer

Documentation

The actual prime stabilizer with its native group structure.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

def nativeResidueStabilizer (B G : Type v) [CommRing B] [Group G]
    [MulSemiringAction G B] (q : Ideal B) : GrpCat.{v}

def

nativeResidueAutomorphisms

L38 ↗

EtaleFundamentalGroups.Inertia.nativeResidueAutomorphisms

Documentation

The actual algebra automorphisms of the literal residue quotient.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

def nativeResidueAutomorphisms (A : Type u) (B : Type v)
    [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p] : GrpCat.{v}

def

nativeResidueStabilizerInclusion

L44 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizerInclusion

Documentation

The original stabilizer inclusion.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

def nativeResidueStabilizerInclusion (B G : Type v) [CommRing B] [Group G]
    [MulSemiringAction G B] (q : Ideal B) : nativeResidueStabilizer B G q →* G

def

nativeResidueStabilizerHom

L49 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizerHom

Documentation

The literal canonical residue homomorphism, retained as its native group map.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

def nativeResidueStabilizerHom (A : Type u) (B G : Type v)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p] :
    nativeResidueStabilizer B G q →* nativeResidueAutomorphisms A B p q

def

nativeResidueStabilizerMorphism

L57 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizerMorphism

Documentation

The same actual map as a native group-category morphism.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · full declaration

def nativeResidueStabilizerMorphism (A : Type u) (B G : Type v)
    [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p] :
    GrpCat.Hom (nativeResidueStabilizer B G q) (nativeResidueAutomorphisms A B p q) where
  hom' := Ideal.Quotient.stabilizerHom q p G

def

nativeResidueAutomorphismRingEquiv

L65 ↗

EtaleFundamentalGroups.Inertia.nativeResidueAutomorphismRingEquiv

Documentation

Forget only the coefficient-linearity proof of the actual automorphism.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

def nativeResidueAutomorphismRingEquiv (A : Type u) (B : Type v)
    [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p]
    (σ : nativeResidueAutomorphisms A B p q) : (B ⧸ q) ≃+* (B ⧸ q)

theorem

nativeQuotientCoefficient_square

L72 ↗

EtaleFundamentalGroups.Inertia.nativeQuotientCoefficient_square

Documentation

The native quotient coefficient square, before an automorphism is introduced.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

theorem nativeQuotientCoefficient_square
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p] :
    (Ideal.Quotient.mk q).comp (algebraMap A B) =
      (algebraMap (A ⧸ p) (B ⧸ q)).comp (Ideal.Quotient.mk p)

theorem

nativeResidueAutomorphismRingEquiv_comp_coefficient

L83 ↗

EtaleFundamentalGroups.Inertia.nativeResidueAutomorphismRingEquiv_comp_coefficient

Documentation

The original quotient-algebra automorphism fixes the actual A coefficients.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

theorem nativeResidueAutomorphismRingEquiv_comp_coefficient
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p]
    (σ : nativeResidueAutomorphisms A B p q) :
    (nativeResidueAutomorphismRingEquiv A B p q σ).toRingHom.comp
        ((Ideal.Quotient.mk q).comp (algebraMap A B)) =
      (Ideal.Quotient.mk q).comp (algebraMap A B)

theorem

nativeResidueAutomorphismRingEquiv_injective

L112 ↗

EtaleFundamentalGroups.Inertia.nativeResidueAutomorphismRingEquiv_injective

Documentation

Forgetting coefficient-linearity does not identify distinct automorphisms.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

theorem nativeResidueAutomorphismRingEquiv_injective
    (A : Type u) (B : Type v) [CommRing A] [CommRing B] [Algebra A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p] :
    Function.Injective (nativeResidueAutomorphismRingEquiv A B p q)

theorem

residueEquation_mem_stabilizer

L123 ↗

EtaleFundamentalGroups.Inertia.residueEquation_mem_stabilizer

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

theorem residueEquation_mem_stabilizer
    {B G : Type v} [CommRing B] [Group G] [MulSemiringAction G B]
    (q : Ideal B) (φ : (B ⧸ q) ≃+* (B ⧸ q)) (g : G)
    (hg : ∀ b : B, (Ideal.Quotient.mk q).toFun (g • b) =
      φ.toRingHom.toFun ((Ideal.Quotient.mk q).toFun b)) :
    g ∈ MulAction.stabilizer G q

def

nativeResidueStabilizerOfEquation

L149 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizerOfEquation

Documentation

The proved global residue equation constructs an actual stabilizer element.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

def nativeResidueStabilizerOfEquation
    {B G : Type v} [CommRing B] [Group G] [MulSemiringAction G B]
    (q : Ideal B) (φ : (B ⧸ q) ≃+* (B ⧸ q)) (g : G)
    (hg : ∀ b : B, (Ideal.Quotient.mk q).toFun (g • b) =
      φ.toRingHom.toFun ((Ideal.Quotient.mk q).toFun b)) :
    nativeResidueStabilizer B G q

theorem

nativeResidueStabilizerOfEquation_value

L158 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizerOfEquation_value

Documentation

The constructed stabilizer element retains its original group element.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

theorem nativeResidueStabilizerOfEquation_value
    {B G : Type v} [CommRing B] [Group G] [MulSemiringAction G B]
    (q : Ideal B) (φ : (B ⧸ q) ≃+* (B ⧸ q)) (g : G)
    (hg : ∀ b : B, (Ideal.Quotient.mk q).toFun (g • b) =
      φ.toRingHom.toFun ((Ideal.Quotient.mk q).toFun b)) :
    (nativeResidueStabilizerInclusion B G q).toFun
      (nativeResidueStabilizerOfEquation q φ g hg) = g

theorem

nativeResidueStabilizerHom_apply_coefficient

L167 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizerHom_apply_coefficient

Documentation

The native residue action has its literal value on original coefficients.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

theorem nativeResidueStabilizerHom_apply_coefficient
    (A : Type u) (B G : Type v) [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p]
    (d : nativeResidueStabilizer B G q) (b : B) :
    (nativeResidueAutomorphismRingEquiv A B p q
      ((nativeResidueStabilizerHom A B G p q).toFun d)).toRingHom.toFun
        ((Ideal.Quotient.mk q).toFun b) =
      (Ideal.Quotient.mk q).toFun ((nativeResidueStabilizerInclusion B G q).toFun d • b)

theorem

nativeResidueStabilizerHom_surjective

L179 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizerHom_surjective

Documentation

The actual native residue action is surjective for the original profinite invariant action. Its lift is constructed by compact residue equations.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

theorem nativeResidueStabilizerHom_surjective
    (A : Type u) (B G : Type v) [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    [Algebra.IsInvariant A B G]
    [TopologicalSpace G] [CompactSpace G] [TotallyDisconnectedSpace G]
    [IsTopologicalGroup G] [TopologicalSpace B] [DiscreteTopology B] [ContinuousSMul G B]
    (p : Ideal A) (q : Ideal B) [q.IsPrime] [q.LiesOver p] :
    Function.Surjective (nativeResidueStabilizerHom A B G p q).toFun

theorem

nativeResidueStabilizerHom_map_ker

L202 ↗

EtaleFundamentalGroups.Inertia.nativeResidueStabilizerHom_map_ker

Documentation

The kernel of the actual residue action, included in the original group, is exactly the original inertia subgroup. This is the native kernel theorem.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open scoped Pointwise
universe u v

Lean source · statement

theorem nativeResidueStabilizerHom_map_ker
    (A : Type u) (B G : Type v) [CommRing A] [CommRing B] [Algebra A B]
    [Group G] [MulSemiringAction G B] [SMulCommClass G A B]
    (p : Ideal A) (q : Ideal B) [q.LiesOver p] :
    (nativeResidueStabilizerHom A B G p q).ker.map
        (nativeResidueStabilizerInclusion B G q) = q.inertia G

Module documentation

The actual native residue-action homomorphism

Declarations