NYLL
Module

IdealTower.lean

Nyll.SchemeTheory.AbhyankarLemma.Geometry.Inertia.IdealTower
5 declarations indexed from sourceView source ↗

Module documentation

Ideal-theoretic inertia in a tower

This file gives the source-level inertia restriction map for a tower of normalizations. It is formulated for equivariant actions on a tower of rings, so it can be instantiated by the integral closures occurring in SGA 1, Expose X, Lemma 3.6.

Imports1
Imported by3

Declarations

def

idealInertiaRestriction

L40 ↗
TameAbhyankar.SGA1.idealInertiaRestriction
Documentation

Restriction of ideal-theoretic inertia along an equivariant tower map.

Source context 14 commands

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

noncomputable section
universe uR uS uT uG uH
namespace TameAbhyankar
namespace SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {R : Type uR} {S : Type uS} {T : Type uT}
variable [CommRing R] [CommRing S] [CommRing T]
variable [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
variable {G : Type uG} {H : Type uH}
variable [Group G] [Group H]
variable [MulSemiringAction G T] [MulSemiringAction H S]
section Restriction
variable (res : G →* H)
variable (P : Ideal S) (Q : Ideal T)
Lean source · full declaration
def idealInertiaRestriction
    [Q.LiesOver P]
    (hres : ∀ sigma : G, ∀ x : S,
      algebraMap S T (res sigma • x) = sigma • algebraMap S T x) :
    Q.toAddSubgroup.inertia G →* P.toAddSubgroup.inertia H where
  toFun sigma := ⟨res sigma, by
    rw [AddSubgroup.mem_inertia]
    intro x
    have htop : sigma • algebraMap S T x - algebraMap S T x ∈ Q :=
      sigma.property (algebraMap S T x)
    have hmap : algebraMap S T (res sigma • x - x) ∈ Q := by
      rw [map_sub, hres]
      exact htop
    have hcomap : res sigma • x - x ∈ Q.comap (algebraMap S T) :=
      hmap
    change res sigma • x - x ∈ P
    rw [Q.over_def P, Ideal.under_def]
    exact hcomap⟩
  map_one' := by
    apply Subtype.ext
    exact res.map_one
  map_mul' sigma tau := by
    apply Subtype.ext
    exact res.map_mul sigma tau
def

idealRelativeInertiaInclusion

L67 ↗
TameAbhyankar.SGA1.idealRelativeInertiaInclusion
Documentation

The relative inertia of the kernel of the restriction homomorphism maps canonically into top inertia.

Source context 14 commands

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

noncomputable section
universe uR uS uT uG uH
namespace TameAbhyankar
namespace SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {R : Type uR} {S : Type uS} {T : Type uT}
variable [CommRing R] [CommRing S] [CommRing T]
variable [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
variable {G : Type uG} {H : Type uH}
variable [Group G] [Group H]
variable [MulSemiringAction G T] [MulSemiringAction H S]
section Restriction
variable (res : G →* H)
variable (P : Ideal S) (Q : Ideal T)
Lean source · full declaration
def idealRelativeInertiaInclusion :
    Q.toAddSubgroup.inertia res.ker →* Q.toAddSubgroup.inertia G where
  toFun sigma := ⟨((sigma : res.ker) : G), sigma.property⟩
  map_one' := rfl
  map_mul' _ _ := rfl
theorem

idealRelativeInertiaInclusion_injective

L74 ↗
TameAbhyankar.SGA1.idealRelativeInertiaInclusion_injective
Documentation

The relative inertia inclusion is injective.

Source context 14 commands

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

noncomputable section
universe uR uS uT uG uH
namespace TameAbhyankar
namespace SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {R : Type uR} {S : Type uS} {T : Type uT}
variable [CommRing R] [CommRing S] [CommRing T]
variable [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
variable {G : Type uG} {H : Type uH}
variable [Group G] [Group H]
variable [MulSemiringAction G T] [MulSemiringAction H S]
section Restriction
variable (res : G →* H)
variable (P : Ideal S) (Q : Ideal T)
Lean source · statement
theorem idealRelativeInertiaInclusion_injective :
    Function.Injective (idealRelativeInertiaInclusion (Q := Q) res)
theorem

idealInertiaRestriction_ker_eq_range_relative

L84 ↗
TameAbhyankar.SGA1.idealInertiaRestriction_ker_eq_range_relative
Documentation

In a tower, relative inertia is exactly the kernel of restriction on inertia groups.

Source context 14 commands

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

noncomputable section
universe uR uS uT uG uH
namespace TameAbhyankar
namespace SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {R : Type uR} {S : Type uS} {T : Type uT}
variable [CommRing R] [CommRing S] [CommRing T]
variable [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
variable {G : Type uG} {H : Type uH}
variable [Group G] [Group H]
variable [MulSemiringAction G T] [MulSemiringAction H S]
section Restriction
variable (res : G →* H)
variable (P : Ideal S) (Q : Ideal T)
Lean source · statement
theorem idealInertiaRestriction_ker_eq_range_relative
    [Q.LiesOver P]
    (hres : ∀ sigma : G, ∀ x : S,
      algebraMap S T (res sigma • x) = sigma • algebraMap S T x) :
    MonoidHom.ker (idealInertiaRestriction res P Q hres) =
      (idealRelativeInertiaInclusion (Q := Q) res).range
theorem

idealInertiaRestriction_surjective

L128 ↗
TameAbhyankar.SGA1.idealInertiaRestriction_surjective
Documentation

For a finite Galois tower with separable residue extensions, restriction on inertia is surjective. The proof is the order calculation used in SGA 1: inertia orders are ramification indices, ramification indices multiply in the tower, and relative inertia is the kernel.

Source context 22 commands

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

noncomputable section
universe uR uS uT uG uH
namespace TameAbhyankar
namespace SGA1
attribute [local instance] Ideal.Quotient.field Module.Free.of_divisionRing
variable {R : Type uR} {S : Type uS} {T : Type uT}
variable [CommRing R] [CommRing S] [CommRing T]
variable [Algebra R S] [Algebra S T] [Algebra R T] [IsScalarTower R S T]
variable {G : Type uG} {H : Type uH}
variable [Group G] [Group H]
variable [MulSemiringAction G T] [MulSemiringAction H S]
section Surjectivity
variable [IsDedekindDomain R] [IsDedekindDomain S] [IsDedekindDomain T]
variable [Module.Finite R S] [Module.Finite S T] [Module.Finite R T]
variable [Module.IsTorsionFree R S] [Module.IsTorsionFree S T]
  [Module.IsTorsionFree R T]
variable [Finite G] [Finite H]
variable (res : G →* H)
variable [IsGaloisGroup G R T] [IsGaloisGroup H R S]
  [IsGaloisGroup res.ker S T]
variable (p : Ideal R) (P : Ideal S) (Q : Ideal T)
variable [p.IsMaximal] [P.IsMaximal] [Q.IsMaximal]
variable [P.LiesOver p] [Q.LiesOver P]
variable [Algebra.IsSeparable (R ⧸ p) (S ⧸ P)]
  [Algebra.IsSeparable (S ⧸ P) (T ⧸ Q)]
Lean source · statement
theorem idealInertiaRestriction_surjective
    (hp : p ≠ ⊥)
    (hres : ∀ sigma : G, ∀ x : S,
      algebraMap S T (res sigma • x) = sigma • algebraMap S T x) :
    Function.Surjective (idealInertiaRestriction res P Q hres)

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