Module

StabilizerLocalizationAction.lean

Nyll.SchemeTheory.RingTheory.Ramification.StabilizerLocalizationAction

11 declarations indexed from sourceView source ↗

Module documentation

Stabilizer actions on prime localizations

Constructs the action of a prime stabilizer on the prime localization and computes it on coefficients. It identifies localization inertia with the original ideal inertia inside the stabilizer.

Imports7

Nyll.SchemeTheory.RingTheory.Ramification.InertiaLocalization
Mathlib.Algebra.Ring.Action.Basic
Mathlib.Algebra.Ring.Action.End
Mathlib.Algebra.Group.Action.End
Mathlib.Algebra.Ring.Equiv
Mathlib.RingTheory.Ideal.Pointwise
Mathlib.RingTheory.Localization.AtPrime.Basic

Imported by14

def

stabilizerCoefficientRingEquiv

L37 ↗

SchemeTheory.stabilizerCoefficientRingEquiv

Documentation

The individual original ring automorphism of a prime stabilizer element.

Source context 8 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]
omit [Q.IsPrime] in

Lean source · statement

def stabilizerCoefficientRingEquiv (σ : MulAction.stabilizer G Q) : B ≃+* B

theorem

stabilizerCoefficientRingEquiv_comap_eq

L43 ↗

SchemeTheory.stabilizerCoefficientRingEquiv_comap_eq

Documentation

The original stabilizer automorphism preserves the actual prime.

Source context 8 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]
omit [Q.IsPrime] in

Lean source · statement

theorem stabilizerCoefficientRingEquiv_comap_eq (σ : MulAction.stabilizer G Q) :
    Q = Q.comap (stabilizerCoefficientRingEquiv B G Q σ).toRingHom

def

stabilizerLocalizationRingEquiv

L53 ↗

SchemeTheory.stabilizerLocalizationRingEquiv

Documentation

The actual stabilizer automorphism on the literal prime localization.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]

Lean source · statement

def stabilizerLocalizationRingEquiv (σ : MulAction.stabilizer G Q) :
    Localization.AtPrime Q ≃+* Localization.AtPrime Q

theorem

stabilizerLocalizationRingEquiv_algebraMap

L58 ↗

SchemeTheory.stabilizerLocalizationRingEquiv_algebraMap

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]

Lean source · statement

theorem stabilizerLocalizationRingEquiv_algebraMap
    (σ : MulAction.stabilizer G Q) (b : B) :
    stabilizerLocalizationRingEquiv B G Q σ (algebraMap B (Localization.AtPrime Q) b) =
      algebraMap B (Localization.AtPrime Q) ((σ : G) • b)

def

stabilizerLocalizationRingAut

L67 ↗

SchemeTheory.stabilizerLocalizationRingAut

Documentation

The actual localization automorphisms preserve identity and composition.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]

Lean source · full declaration

def stabilizerLocalizationRingAut :
    MulAction.stabilizer G Q →* (Localization.AtPrime Q ≃+* Localization.AtPrime Q) where
  toFun := stabilizerLocalizationRingEquiv B G Q
  map_one' := by
    apply RingEquiv.toRingHom_injective
    apply IsLocalization.ringHom_ext Q.primeCompl
    apply RingHom.ext
    intro b
    change stabilizerLocalizationRingEquiv B G Q 1
      (algebraMap B (Localization.AtPrime Q) b) = algebraMap B (Localization.AtPrime Q) b
    rw [stabilizerLocalizationRingEquiv_algebraMap]
    exact congrArg (algebraMap B (Localization.AtPrime Q)) (one_smul G b)
  map_mul' σ τ := by
    apply RingEquiv.toRingHom_injective
    apply IsLocalization.ringHom_ext Q.primeCompl
    apply RingHom.ext
    intro b
    change stabilizerLocalizationRingEquiv B G Q (σ * τ)
        (algebraMap B (Localization.AtPrime Q) b) =
      stabilizerLocalizationRingEquiv B G Q σ
        (stabilizerLocalizationRingEquiv B G Q τ
          (algebraMap B (Localization.AtPrime Q) b))
    rw [stabilizerLocalizationRingEquiv_algebraMap,
      stabilizerLocalizationRingEquiv_algebraMap,
      stabilizerLocalizationRingEquiv_algebraMap]
    exact congrArg (algebraMap B (Localization.AtPrime Q)) (mul_smul (σ : G) (τ : G) b)

instance

stabilizerLocalizationMulSemiringAction

L95 ↗

SchemeTheory.stabilizerLocalizationMulSemiringAction

Documentation

The canonical actual decomposition-group action on the prime localization.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]

Lean source · statement

instance stabilizerLocalizationMulSemiringAction :
    MulSemiringAction (MulAction.stabilizer G Q) (Localization.AtPrime Q)

theorem

stabilizerLocalization_smul_algebraMap

L99 ↗

SchemeTheory.stabilizerLocalization_smul_algebraMap

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]

Lean source · statement

theorem stabilizerLocalization_smul_algebraMap
    (σ : MulAction.stabilizer G Q) (b : B) :
    σ • algebraMap B (Localization.AtPrime Q) b =
      algebraMap B (Localization.AtPrime Q) ((σ : G) • b)

theorem

stabilizerLocalizationRingEquiv_eq_inertiaLocalizationRingEquiv

L107 ↗

SchemeTheory.stabilizerLocalizationRingEquiv_eq_inertiaLocalizationRingEquiv

Documentation

The canonical action agrees with the already constructed individual inertia-localization automorphism.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]

Lean source · statement

theorem stabilizerLocalizationRingEquiv_eq_inertiaLocalizationRingEquiv
    (σ : MulAction.stabilizer G Q) (hσ : (σ : G) ∈ Q.inertia G) :
    stabilizerLocalizationRingEquiv B G Q σ =
      inertiaLocalizationRingEquiv B Q (stabilizerCoefficientRingEquiv B G Q σ) hσ

theorem

inertiaLocalizationRingEquiv_sub_mem_maximalIdeal

L113 ↗

SchemeTheory.inertiaLocalizationRingEquiv_sub_mem_maximalIdeal

Source context 8 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]
omit [Group G] [MulSemiringAction G B] in

Lean source · statement

theorem inertiaLocalizationRingEquiv_sub_mem_maximalIdeal
    (σ : B ≃+* B) (hσ : ∀ b : B, σ b - b ∈ Q) (x : Localization.AtPrime Q) :
    inertiaLocalizationRingEquiv B Q σ hσ x - x ∈
      IsLocalRing.maximalIdeal (Localization.AtPrime Q)

theorem

stabilizerLocalization_mem_inertia_iff

L127 ↗

SchemeTheory.stabilizerLocalization_mem_inertia_iff

Documentation

Actual localization inertia is exactly original ideal inertia inside the actual prime stabilizer.

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]

Lean source · statement

theorem stabilizerLocalization_mem_inertia_iff (σ : MulAction.stabilizer G Q) :
    σ ∈ (IsLocalRing.maximalIdeal (Localization.AtPrime Q)).inertia (MulAction.stabilizer G Q) ↔
      (σ : G) ∈ Q.inertia G

theorem

stabilizerLocalization_inertia_eq

L145 ↗

SchemeTheory.stabilizerLocalization_inertia_eq

Source context 7 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v
variable (B : Type u) [CommRing B]
variable (G : Type v) [Group G] [MulSemiringAction G B]
variable (Q : Ideal B) [Q.IsPrime]

Lean source · statement

theorem stabilizerLocalization_inertia_eq :
    (IsLocalRing.maximalIdeal (Localization.AtPrime Q)).inertia (MulAction.stabilizer G Q) =
      (Q.inertia G).subgroupOf (MulAction.stabilizer G Q)

Module documentation

Stabilizer actions on prime localizations

Declarations