NYLL
Module

InertiaFixedIntegralMultiple.lean

Nyll.SchemeTheory.RingTheory.Ramification.InertiaFixedIntegralMultiple
1 declaration indexed from sourceView source ↗

Module documentation

Inertia-fixed integral numerators

For an element of the ambient Galois field fixed by normalization inertia, the native integral-multiple theorem supplies a nonzero base denominator. Scalar preservation and the existing literal coefficient square prove that the resulting actual integral-closure numerator is fixed by the same original inertia. No finite extension, fixed-field comparison, or stalk-image premise is introduced. The base denominator need not avoid the prime.

Imports5
Imported by2

Declarations

theorem

integralClosure_exists_inertia_fixed_integral_multiple

L35 ↗
EtaleFundamentalGroups.Inertia.integralClosure_exists_inertia_fixed_integral_multiple
Documentation

An original inertia-fixed field element has an inertia-fixed integral numerator after multiplication by a nonzero element of the original base. The statement holds for any ideal; in particular for the original prime.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
universe u v w
attribute [local instance] normalizationInertiaImageAction
Lean source · statement
theorem integralClosure_exists_inertia_fixed_integral_multiple
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra K L] [Algebra A L]
    [IsScalarTower A K L] [IsGalois K L]
    (Q : Ideal (integralClosure A L)) (x : L)
    (hx : ∀ σ ∈ Q.inertia Gal(L/K), σ x = x) :
    ∃ a : A, a ≠ 0 ∧ ∃ b : integralClosure A L,
      (b : L) = a • x ∧ ∀ σ ∈ Q.inertia Gal(L/K), σ • b = b

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