NYLL
Module

FiniteNormalizationInertiaLift.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteNormalizationInertiaLift
2 declarations indexed from sourceView source ↗

Module documentation

Lifting normalization inertia to finite fields

Transfers the inertia difference condition through normalization restriction and lifts intrinsic finite-normalization inertia to finite-field inertia.

Imports2
Imported by2

Declarations

theorem

mem_inertia_of_normalization_restriction

L32 ↗
EtaleFundamentalGroups.Inertia.mem_inertia_of_normalization_restriction
Documentation

Actual equality with the normalization restriction transfers the literal inertia difference condition to the prescribed field action. This action comparison does not introduce finite-dimensional module data.

Source context 6 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
section NativeRestriction
attribute [local instance] normalizationCommAlgGaloisAction
Lean source · statement
theorem mem_inertia_of_normalization_restriction
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F] [IsGalois K F]
    (Q : Ideal (normalizationCommAlgCat A F).carrier) (σ : F ≃ₐ[K] F)
    (τ : (normalizationCommAlgCat A F).carrier ≃ₐ[A] (normalizationCommAlgCat A F).carrier)
    (hσ : (σ.restrictScalars A).mapIntegralClosure = τ)
    (hτ : ∀ b : (normalizationCommAlgCat A F).carrier, τ.toRingHom.toFun b - b ∈ Q) :
    σ ∈ Q.inertia Gal(F/K)
theorem

finiteNormalization_inertia_exists_field_lift

L60 ↗
EtaleFundamentalGroups.Inertia.finiteNormalization_inertia_exists_field_lift
Documentation

An intrinsic finite-normalization inertia automorphism lifts to the prescribed finite-field ideal inertia. Its restriction is the same actual coefficient automorphism, not a separately supplied comparison.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
Lean source · statement
theorem finiteNormalization_inertia_exists_field_lift
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K F] [Algebra A F] [IsScalarTower A K F]
    [IsGalois K F] [FiniteDimensional K F]
    (Q : Ideal (integralClosure A F))
    (τ : integralClosure A F ≃ₐ[A] integralClosure A F)
    (hτ : ∀ b : integralClosure A F, τ.toRingHom b - b ∈ Q) :
    ∃ σ : F ≃ₐ[K] F,
      σ ∈ Q.inertia Gal(F/K) ∧ (σ.restrictScalars A).mapIntegralClosure = τ

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