Module

AlgebraicRamificationDetection.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.AlgebraicRamificationDetection

1 declaration indexed from sourceView source ↗

Module documentation

Detecting absolute ramification on finite Galois layers

For an actual inertia element, ramification can be tested after restriction to every finite Galois intermediate field. A failure of the defining principal-unit condition involves one unit, which already lies in one such finite layer. No Henselianity or residue-characteristic hypothesis is used.

Imports3

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.BaseChange
Nyll.ValuedFieldTheory.Valuation.ComapResidueCharacteristic
Mathlib.FieldTheory.Galois.Profinite

Imported by3

theorem

mem_ramificationGroup_iff_forall_finiteGalois_restrict

L28 ↗

RamificationTheory.HilbertRamification.ValuationSubring.mem_ramificationGroup_iff_forall_finiteGalois_restrict

Documentation

Membership in actual ramification, inside inertia, is equivalent to ramification of all finite Galois restrictions in their ambient automorphism groups. This is the finite-coordinate membership test used on compact inertia.

Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.ValuationSubring
universe u v

Lean source · statement

theorem mem_ramificationGroup_iff_forall_finiteGalois_restrict
    (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [IsGalois K L]
    (A : _root_.ValuationSubring L) (σ : inertiaGroup K A) :
    σ ∈ ramificationGroup K A ↔
      ∀ E : FiniteGaloisIntermediateField K L,
        AlgEquiv.restrictNormalHom (F := K) (K₁ := L) E
            (inertiaGroupToAut (K := K) A σ) ∈
          ramificationGroupInAut K (A.comap E.toIntermediateField.val.toRingHom)

Module documentation

Detecting absolute ramification on finite Galois layers

Declarations

mem_ramificationGroup_iff_forall_finiteGalois_restrict