Module

CommAlgDecompositionGroup.lean

Nyll.EtaleFundamentalGroups.Inertia.CommAlgDecompositionGroup

6 declarations indexed from sourceView source ↗

Module documentation

Native coefficient decomposition groups

The group is the existing native residue stabilizer, with the existing coefficient-automorphism action. Ring-only contraction and action comparison prove the stability and lifting statements used by actual finite restrictions.

Imports5

Nyll.SchemeTheory.RingTheory.Ramification.NativeResidueAction
Nyll.SchemeTheory.RingTheory.Ramification.StabilizerLocalizationAction
Nyll.SchemeTheory.Normalization.NativeAutomorphismRingMaps
Mathlib.RingTheory.Ideal.Maps
Mathlib.RingTheory.Ideal.Pointwise

Imported by9

def

commAlgIdealDecompositionGroup

L32 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealDecompositionGroup

Documentation

The existing coefficient-automorphism stabilizer, owned by its native coefficient algebra so finite towers do not reopen its action dictionaries.

Source context 5 commands

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

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

Lean source · statement

def commAlgIdealDecompositionGroup (A : Type u) [CommRing A]
    (B : CommAlgCat.{v} A) (Q : Ideal B.carrier) : GrpCat.{v}

theorem

commAlgIdealDecomposition_comap

L38 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealDecomposition_comap

Documentation

The native coefficient ring map of a stabilizer element fixes the literal prime under contraction. The action dictionaries stay in this owner.

Source context 5 commands

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

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

Lean source · statement

theorem commAlgIdealDecomposition_comap
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B.carrier)
    (σ : (commAlgIdealDecompositionGroup A B Q).carrier) :
    Q = Q.comap (commAlgAutomorphismRingHom A B σ.val)

theorem

ideal_map_comap_eq_of_equivariant

L45 ↗

EtaleFundamentalGroups.Inertia.ideal_map_comap_eq_of_equivariant

Documentation

An equivariant literal ring map contracts a fixed ideal to a fixed ideal.

Source context 5 commands

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

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

Lean source · statement

theorem ideal_map_comap_eq_of_equivariant
    (B : Type v) (C : Type w) [CommRing B] [CommRing C]
    (j : B →+* C) (s : B ≃+* B) (t : C ≃+* C) (Q : Ideal C)
    (hcomm : j.comp s.toRingHom = t.toRingHom.comp j)
    (hQ : Q = Q.comap t.toRingHom) :
    (Q.comap j).map s.toRingHom = Q.comap j

def

commAlgDecompositionHomOfStabilizer

L63 ↗

EtaleFundamentalGroups.Inertia.commAlgDecompositionHomOfStabilizer

Documentation

Actual coefficient stability constructs a morphism into the existing native decomposition group.

Source context 5 commands

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

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

Lean source · full declaration

def commAlgDecompositionHomOfStabilizer
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (G : GrpCat.{v})
    (Q : Ideal B.carrier) (f : GrpCat.Hom G (commAlgAutomorphismGroup A B))
    (hf : ∀ g : G.carrier,
      Q.map (commAlgAutomorphismRingHom A B (f.hom'.toFun g)) = Q) :
    GrpCat.Hom G (commAlgIdealDecompositionGroup A B Q) where
  hom' :=
    { toFun := fun g => ⟨f.hom'.toFun g, hf g⟩
      map_one' := Subtype.ext f.hom'.map_one
      map_mul' := fun g h => Subtype.ext (f.hom'.map_mul g h) }

theorem

commAlgIdealDecomposition_eq_one_iff_coefficient

L76 ↗

EtaleFundamentalGroups.Inertia.commAlgIdealDecomposition_eq_one_iff_coefficient

Documentation

A native stabilizer element is trivial exactly when its coefficient ring map is the identity.

Source context 5 commands

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

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

Lean source · statement

theorem commAlgIdealDecomposition_eq_one_iff_coefficient
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (Q : Ideal B.carrier)
    (σ : (commAlgIdealDecompositionGroup A B Q).carrier) :
    σ = 1 ↔ commAlgAutomorphismRingHom A B σ.val = RingHom.id B.carrier

theorem

coefficientDecomposition_exists_preimage

L92 ↗

EtaleFundamentalGroups.Inertia.coefficientDecomposition_exists_preimage

Documentation

An actual coefficient-automorphism lift with the same ring action preserves the literal ideal stabilizer condition.

Source context 5 commands

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

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

Lean source · full declaration

theorem coefficientDecomposition_exists_preimage
    (A : Type u) [CommRing A] (B : CommAlgCat.{v} A) (G : GrpCat.{v})
    (Q : Ideal B.carrier) (a : MulSemiringAction G.carrier B.carrier)
    (f : GrpCat.Hom G (commAlgAutomorphismGroup A B))
    (hsurj : Function.Surjective f.hom'.toFun)
    (hcompare :
      let : MulSemiringAction G.carrier B.carrier := a
      ∀ g : G.carrier, MulSemiringAction.toRingHom G.carrier B.carrier g =
        commAlgAutomorphismRingHom A B (f.hom'.toFun g)) :
    let : MulSemiringAction G.carrier B.carrier := a
    ∀ τ : (commAlgIdealDecompositionGroup A B Q).carrier,
      ∃ g : G.carrier, (MulAction.stabilizer G.carrier Q).carrier g ∧
        f.hom'.toFun g = τ.val := by
  intro ringAction τ
  obtain ⟨g, hg⟩ := hsurj τ.val
  refine ⟨g, ?_, hg⟩
  change Q.map (MulSemiringAction.toRingHom G.carrier B.carrier g) = Q
  rw [hcompare g, hg]
  exact τ.property

Module documentation

Native coefficient decomposition groups

Declarations

commAlgIdealDecompositionGroup

commAlgIdealDecomposition_comap

ideal_map_comap_eq_of_equivariant

commAlgDecompositionHomOfStabilizer

commAlgIdealDecomposition_eq_one_iff_coefficient

coefficientDecomposition_exists_preimage