Module

InertiaLocalization.lean

Nyll.SchemeTheory.RingTheory.Ramification.InertiaLocalization

5 declarations indexed from sourceView source ↗

Module documentation

Individual inertia automorphisms on the literal prime localization

The native inertia-to-stabilizer theorem supplies preservation of the prime, then the native local-ring equivalence extends the original automorphism. Its coefficient formula proves compatibility with the original base map. Native localization extensionality and maximal-ideal contraction prove that its residue action is the identity. No group action on the localization is introduced, and no valuation or finiteness hypothesis is required.

Imports7

Mathlib.Algebra.Algebra.Equiv
Mathlib.Algebra.Ring.Action.Group
Mathlib.RingTheory.Ideal.Pointwise
Mathlib.RingTheory.Ideal.Quotient.Defs
Mathlib.RingTheory.Localization.AtPrime.Basic
Mathlib.RingTheory.Localization.Defs
Mathlib.RingTheory.LocalRing.ResidueField.Basic

Imported by5

theorem

inertia_comap_eq

L34 ↗

SchemeTheory.inertia_comap_eq

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v

Lean source · statement

theorem inertia_comap_eq
    (B : Type u) [CommRing B] (Q : Ideal B) (σ : B ≃+* B)
    (hσ : ∀ b : B, σ b - b ∈ Q) : Q = Q.comap σ.toRingHom

def

inertiaLocalizationRingEquiv

L43 ↗

SchemeTheory.inertiaLocalizationRingEquiv

Documentation

Extend an actual inertia automorphism to the literal localization at Q.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v

Lean source · statement

def inertiaLocalizationRingEquiv
    (B : Type u) [CommRing B] (Q : Ideal B) [Q.IsPrime] (σ : B ≃+* B)
    (hσ : ∀ b : B, σ b - b ∈ Q) :
    Localization.AtPrime Q ≃+* Localization.AtPrime Q

theorem

inertiaLocalizationRingEquiv_algebraMap

L50 ↗

SchemeTheory.inertiaLocalizationRingEquiv_algebraMap

Documentation

The native localization extension has the original value on coefficients.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v

Lean source · statement

theorem inertiaLocalizationRingEquiv_algebraMap
    (B : Type u) [CommRing B] (Q : Ideal B) [Q.IsPrime] (σ : B ≃+* B)
    (hσ : ∀ b : B, σ b - b ∈ Q) (b : B) :
    inertiaLocalizationRingEquiv B Q σ hσ (algebraMap B (Localization.AtPrime Q) b) =
      algebraMap B (Localization.AtPrime Q) (σ b)

theorem

inertiaLocalizationRingEquiv_comp_baseMap

L60 ↗

SchemeTheory.inertiaLocalizationRingEquiv_comp_baseMap

Documentation

A commuting original ring map remains fixed after localization. This interface uses the literal ring map and its supplied commutation proof, so no extra base-algebra action is opened at a dense Galois boundary.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v

Lean source · statement

theorem inertiaLocalizationRingEquiv_comp_baseMap
    (A : Type u) (B : Type v) [CommRing A] [CommRing B]
    (Q : Ideal B) [Q.IsPrime] (σ : B ≃+* B)
    (hσ : ∀ b : B, σ b - b ∈ Q) (f : A →+* B)
    (hf : σ.toRingHom.comp f = f) :
    (inertiaLocalizationRingEquiv B Q σ hσ).toRingHom.comp
        ((algebraMap B (Localization.AtPrime Q)).comp f) =
      (algebraMap B (Localization.AtPrime Q)).comp f

theorem

inertiaLocalizationRingEquiv_comp_residue

L75 ↗

SchemeTheory.inertiaLocalizationRingEquiv_comp_residue

Documentation

The extended individual inertia automorphism acts trivially on the actual residue field of the prime localization. Prime Q need not be maximal in B.

Source context 4 commands

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

noncomputable section
open scoped Pointwise
namespace SchemeTheory
universe u v

Lean source · statement

theorem inertiaLocalizationRingEquiv_comp_residue
    (B : Type u) [CommRing B] (Q : Ideal B) [Q.IsPrime] (σ : B ≃+* B)
    (hσ : ∀ b : B, σ b - b ∈ Q) :
    (IsLocalRing.residue (Localization.AtPrime Q)).comp
        (inertiaLocalizationRingEquiv B Q σ hσ).toRingHom =
      IsLocalRing.residue (Localization.AtPrime Q)

Module documentation

Individual inertia automorphisms on the literal prime localization

Declarations

inertia_comap_eq

inertiaLocalizationRingEquiv

inertiaLocalizationRingEquiv_algebraMap

inertiaLocalizationRingEquiv_comp_baseMap

inertiaLocalizationRingEquiv_comp_residue