Module

HenselianResidueScalars.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.HenselianResidueScalars

3 declarations indexed from sourceView source ↗

Module documentation

Actual residue scalars in the Henselian decomposition sequence

The residue field of the fixed integer ring and the actual residue field of an intermediate field have the same image in the selected residue field. The comparison is proved on integer representatives. It does not assume an identification of residue fields or separability of residue extensions.

Imports5

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.HenselianDecomposition
Nyll.ValuedFieldTheory.Valuation.Henselian.UniqueExtensionReduction
Nyll.ValuedFieldTheory.Valuation.UniqueRing
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Valuation.Extension

Imported by2

theorem

intermediateFieldComap_hasExtension

L30 ↗

RamificationTheory.HilbertRamification.ValuationSubring.intermediateFieldComap_hasExtension

Documentation

The selected valuation extends the canonical valuation of its actual pullback to an intermediate field.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem intermediateFieldComap_hasExtension
    (A : _root_.ValuationSubring L) (E : IntermediateField K L) :
    (A.comap E.val.toRingHom).valuation.HasExtension A.valuation

theorem

decompositionResidue_algebraMap_mk

L39 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionResidue_algebraMap_mk

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem decompositionResidue_algebraMap_mk
    (A : _root_.ValuationSubring L) (E : IntermediateField K L)
    (a : decompositionFixedSubring E A) :
    algebraMap (decompositionResidueField E A) (selectedResidueField A)
        (Ideal.Quotient.mk (decompositionFixedMaximalIdeal E A) a) =
      IsLocalRing.residue A (a : A)

theorem

decompositionResidue_scalar_range_eq_comap_residueMap_of_henselianRing

L50 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionResidue_scalar_range_eq_comap_residueMap_of_henselianRing

Documentation

In the residue exact sequence over an intermediate field, the intrinsic base scalars have exactly the image of the actual intermediate residue field. Henselianity supplies the fixed-integer descent used in this comparison.

Source context 3 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v
variable {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem decompositionResidue_scalar_range_eq_comap_residueMap_of_henselianRing
    [IsGalois K L]
    (V : _root_.ValuationSubring K)
    [HenselianRing V (IsLocalRing.maximalIdeal V)]
    (A : _root_.ValuationSubring L) [V.valuation.HasExtension A.valuation]
    (E : IntermediateField K L) :
    Set.range (algebraMap (decompositionResidueField E A) (selectedResidueField A)) =
      Set.range (ValuationTheory.Valuations.residueFieldMapOfHasExtension
        (A.comap E.val.toRingHom) A (intermediateFieldComap_hasExtension A E))

Module documentation

Actual residue scalars in the Henselian decomposition sequence

Declarations

intermediateFieldComap_hasExtension

decompositionResidue_algebraMap_mk

decompositionResidue_scalar_range_eq_comap_residueMap_of_henselianRing