Module

ResidueExactSequence.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.ResidueExactSequence

34 declarations indexed from sourceView source ↗

Module documentation

The residue-action exact sequence

For a (possibly infinite) Galois extension and a chosen extension valuation, the residue extension over the decomposition field is normal and reduction gives the exact sequence

1 → I_w → G_w → Gal(λ/κ) → 1.

The base residue field is presented intrinsically as the quotient of the fixed subring of the chosen valuation ring by the contraction of its maximal ideal. This fixed subring is exactly the valuation ring on the decomposition field. The profinite surjectivity proof is the compact inverse-limit argument used in this construction, supplied by Ideal.Quotient.stabilizerHom_surjective_of_profinite.

Imports2

Imported by6

abbrev

decompositionFixedSubring

L44 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedSubring

Documentation

The valuation ring on the decomposition field, represented inside the chosen valuation ring as the fixed subring of the decomposition group.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

abbrev decompositionFixedSubring (A : _root_.ValuationSubring L) : Subring A

abbrev

decompositionFixedMaximalIdeal

L48 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedMaximalIdeal

Documentation

The maximal ideal of the decomposition-field valuation ring.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

abbrev decompositionFixedMaximalIdeal (A : _root_.ValuationSubring L) :
    Ideal (decompositionFixedSubring K A)

abbrev

decompositionResidueField

L53 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionResidueField

Documentation

The actual base residue field κ in the residue-action exact sequence.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

abbrev decompositionResidueField (A : _root_.ValuationSubring L)

abbrev

selectedResidueField

L57 ↗

RamificationTheory.HilbertRamification.ValuationSubring.selectedResidueField

Documentation

The actual target residue field λ.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

abbrev selectedResidueField (A : _root_.ValuationSubring L)

abbrev

decompositionFieldValuationSubring

L61 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFieldValuationSubring

Documentation

The literal valuation ring on the classical decomposition field Z_w.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

abbrev decompositionFieldValuationSubring
    (A : _root_.ValuationSubring L) :
    _root_.ValuationSubring (decompositionField K A)

def

decompositionFieldValuationSubringEquivFixedSubring

L68 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFieldValuationSubringEquivFixedSubring

Documentation

The fixed-subring presentation used in the residue-action exact sequence is canonically the literal valuation ring on Z_w.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · full declaration

def decompositionFieldValuationSubringEquivFixedSubring
    (A : _root_.ValuationSubring L) :
    decompositionFieldValuationSubring K A ≃+*
      decompositionFixedSubring K A where
  toFun z :=
    ⟨⟨((z : decompositionField K A) : L), z.property⟩, by
      intro sigma
      apply Subtype.ext
      change ((sigma : decompositionGroup K A) : L ≃ₐ[K] L)
          ((z : decompositionField K A) : L) =
        ((z : decompositionField K A) : L)
      exact (IntermediateField.mem_fixedField_iff
        (H := decompositionGroup K A) ((z : decompositionField K A) : L)).mp
          (z : decompositionField K A).property
          (sigma : L ≃ₐ[K] L) sigma.property⟩
  invFun r := by
    let z : decompositionField K A :=
      ⟨((r : A) : L), by
        rw [IntermediateField.mem_fixedField_iff]
        intro sigma hsigma
        have hr := r.property ⟨sigma, hsigma⟩
        exact congrArg Subtype.val hr⟩
    exact ⟨z, r.val.property⟩
  left_inv z := by ext; rfl
  right_inv r := by ext; rfl
  map_add' _ _ := by ext; rfl
  map_mul' _ _ := by ext; rfl

instance

instIsLocalRing

L97 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedSubring.instIsLocalRing

Documentation

Provides the instance instIsLocalRing.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

instance decompositionFixedSubring.instIsLocalRing
    (A : _root_.ValuationSubring L) :
    IsLocalRing (decompositionFixedSubring K A)

theorem

decompositionGroup_action_locallyConstant

L102 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup_action_locallyConstant

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · full declaration

theorem decompositionGroup_action_locallyConstant
    (A : _root_.ValuationSubring L) (a : A) :
    IsLocallyConstant (fun g : decompositionGroup K A ↦ g • a) := by
  rw [IsLocallyConstant.iff_exists_open]
  intro sigma
  let E : IntermediateField K L := IntermediateField.adjoin K {(a : L)}
  let : FiniteDimensional K E :=
    IntermediateField.adjoin.finiteDimensional
      (Algebra.IsIntegral.isIntegral (a : L))
  let U : Set (decompositionGroup K A) :=
    ((↑) : decompositionGroup K A → (L ≃ₐ[K] L)) ⁻¹'
      (((sigma : L ≃ₐ[K] L)) • (E.fixingSubgroup : Set (L ≃ₐ[K] L)))
  refine ⟨U, E.fixingSubgroup_isOpen.smul
      (sigma : L ≃ₐ[K] L) |>.preimage continuous_subtype_val, ?_, ?_⟩
  · exact ⟨1, E.fixingSubgroup.one_mem, by simp⟩
  · intro tau htau
    rcases htau with ⟨g, hg, heq⟩
    have hga : g (a : L) = (a : L) :=
      (IntermediateField.mem_fixingSubgroup_iff E g).mp hg (a : L)
        (IntermediateField.subset_adjoin (F := K) (S := {(a : L)}) (by simp))
    apply Subtype.ext
    change (((tau : decompositionGroup K A) : L ≃ₐ[K] L) (a : L)) =
      (((sigma : decompositionGroup K A) : L ≃ₐ[K] L) (a : L))
    rw [← heq]
    simp [AlgEquiv.mul_apply, hga]

theorem

decompositionGroup_continuousSMul

L128 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup_continuousSMul

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · full declaration

theorem decompositionGroup_continuousSMul
    (A : _root_.ValuationSubring L) :
    letI : TopologicalSpace A := ⊥
    ContinuousSMul (decompositionGroup K A) A := by
  let : TopologicalSpace A := ⊥
  let : DiscreteTopology A := ⟨rfl⟩
  constructor
  rw [continuous_prod_of_discrete_right]
  intro a
  exact (decompositionGroup_action_locallyConstant (K := K) A a).continuous

theorem

decompositionGroup_compactSpace

L139 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup_compactSpace

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

theorem decompositionGroup_compactSpace
    (A : _root_.ValuationSubring L) :
    CompactSpace (decompositionGroup K A)

theorem

decompositionFixedSubring_smulCommClass

L147 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedSubring_smulCommClass

Source context 9 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem decompositionFixedSubring_smulCommClass
    (A : _root_.ValuationSubring L) :
    SMulCommClass (decompositionGroup K A)
      (decompositionFixedSubring K A) A

theorem

decompositionFixedSubring_isInvariant

L157 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedSubring_isInvariant

Source context 9 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem decompositionFixedSubring_isInvariant
    (A : _root_.ValuationSubring L) :
    Algebra.IsInvariant (decompositionFixedSubring K A) A
      (decompositionGroup K A)

instance

instSMulCommClass

L166 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedSubring.instSMulCommClass

Documentation

Provides the instance instSMulCommClass.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

instance decompositionFixedSubring.instSMulCommClass
    (A : _root_.ValuationSubring L) :
    SMulCommClass (decompositionGroup K A)
      (decompositionFixedSubring K A) A

instance

instIsInvariant

L173 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedSubring.instIsInvariant

Documentation

Provides the instance instIsInvariant.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

instance decompositionFixedSubring.instIsInvariant
    (A : _root_.ValuationSubring L) :
    Algebra.IsInvariant (decompositionFixedSubring K A) A
      (decompositionGroup K A)

theorem

decompositionFixedMaximalIdeal_isMaximal

L179 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedMaximalIdeal_isMaximal

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

theorem decompositionFixedMaximalIdeal_isMaximal
    (A : _root_.ValuationSubring L) :
    (decompositionFixedMaximalIdeal K A).IsMaximal

instance

instIsMaximal

L203 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedMaximalIdeal.instIsMaximal

Documentation

Provides the instance instIsMaximal.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

instance decompositionFixedMaximalIdeal.instIsMaximal
    (A : _root_.ValuationSubring L) :
    (decompositionFixedMaximalIdeal K A).IsMaximal

theorem

decompositionFixedMaximalIdeal_eq_maximalIdeal

L210 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFixedMaximalIdeal_eq_maximalIdeal

Documentation

The contracted ideal used in the intrinsic presentation is the actual maximal ideal of the valuation ring on Z_w.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

theorem decompositionFixedMaximalIdeal_eq_maximalIdeal
    (A : _root_.ValuationSubring L) :
    decompositionFixedMaximalIdeal K A =
      IsLocalRing.maximalIdeal (decompositionFixedSubring K A)

def

decompositionFieldResidueEquiv

L219 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFieldResidueEquiv

Documentation

Canonical identification of the literal residue field of Z_w with the base residue field used by the residue-action exact sequence.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

def decompositionFieldResidueEquiv
    (A : _root_.ValuationSubring L) :
    IsLocalRing.ResidueField (decompositionFieldValuationSubring K A) ≃+*
      decompositionResidueField K A

instance

instLiesOver

L229 ↗

RamificationTheory.HilbertRamification.ValuationSubring.selectedMaximalIdeal.instLiesOver

Documentation

Provides the instance instLiesOver.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

instance selectedMaximalIdeal.instLiesOver
    (A : _root_.ValuationSubring L) :
    (IsLocalRing.maximalIdeal A).LiesOver
      (decompositionFixedMaximalIdeal K A)

instance

instField

L237 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionResidueField.instField

Documentation

Provides the instance instField.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

instance decompositionResidueField.instField
    (A : _root_.ValuationSubring L) :
    Field (decompositionResidueField K A)

instance

instAlgebra

L243 ↗

RamificationTheory.HilbertRamification.ValuationSubring.selectedResidueField.instAlgebra

Documentation

Provides the instance instAlgebra.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

instance selectedResidueField.instAlgebra
    (A : _root_.ValuationSubring L) :
    Algebra (decompositionResidueField K A) (selectedResidueField A)

theorem

decompositionGroup_maximalIdeal_stabilizer_eq_top

L253 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroup_maximalIdeal_stabilizer_eq_top

Documentation

Every decomposition-group automorphism stabilizes the maximal ideal of the selected valuation ring.

Source context 9 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem decompositionGroup_maximalIdeal_stabilizer_eq_top
    (A : _root_.ValuationSubring L) :
    MulAction.stabilizer (decompositionGroup K A)
        (IsLocalRing.maximalIdeal A) = ⊤

def

decompositionGroupToMaximalIdealStabilizer

L276 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupToMaximalIdealStabilizer

Documentation

The canonical identification of the decomposition group with the stabilizer of the selected maximal ideal.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · full declaration

def decompositionGroupToMaximalIdealStabilizer
    (A : _root_.ValuationSubring L) :
    decompositionGroup K A →*
      MulAction.stabilizer (decompositionGroup K A)
        (IsLocalRing.maximalIdeal A) where
  toFun sigma := ⟨sigma, by
    rw [decompositionGroup_maximalIdeal_stabilizer_eq_top (K := K) A]
    exact Subgroup.mem_top sigma⟩
  map_one' := rfl
  map_mul' _ _ := rfl

def

decompositionGroupResidueAction

L288 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction

Documentation

The residue-action exact sequence: the residue action of G_w on λ/κ.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

def decompositionGroupResidueAction
    (A : _root_.ValuationSubring L) :
    decompositionGroup K A →*
      (selectedResidueField A ≃ₐ[decompositionResidueField K A]
        selectedResidueField A)

theorem

decompositionGroupResidueAction_residue

L301 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction_residue

Documentation

States the theorem decompositionGroupResidueAction_residue.

Source context 9 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem decompositionGroupResidueAction_residue
    (A : _root_.ValuationSubring L)
    (sigma : decompositionGroup K A) (x : A) :
    decompositionGroupResidueAction (K := K) A sigma
        (IsLocalRing.residue A x) =
      IsLocalRing.residue A (sigma • x)

def

decompositionFieldResidueMapToSelected

L312 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionFieldResidueMapToSelected

Documentation

The canonical embedding of the literal residue field of Z_w into the selected residue field λ; it is the usual residue map, expressed through the canonical fixed-subring comparison.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

def decompositionFieldResidueMapToSelected
    (A : _root_.ValuationSubring L) :
    IsLocalRing.ResidueField (decompositionFieldValuationSubring K A) →+*
      selectedResidueField A

theorem

decompositionGroupResidueAction_commutes_decompositionFieldResidue

L323 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction_commutes_decompositionFieldResidue

Documentation

The residue action in the exact sequence fixes the actual residue field of the decomposition field. This is the action-compatibility part of the bridge from the intrinsic quotient presentation to the classical λ/κ.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

theorem decompositionGroupResidueAction_commutes_decompositionFieldResidue
    (A : _root_.ValuationSubring L)
    (sigma : decompositionGroup K A)
    (x : IsLocalRing.ResidueField
      (decompositionFieldValuationSubring K A)) :
    decompositionGroupResidueAction (K := K) A sigma
        (decompositionFieldResidueMapToSelected (K := K) A x) =
      decompositionFieldResidueMapToSelected (K := K) A x

theorem

decompositionGroupResidueAction_ker

L336 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction_ker

Documentation

The residue-action homomorphism has the ordinary inertia group as kernel.

Source context 9 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem decompositionGroupResidueAction_ker
    (A : _root_.ValuationSubring L) :
    MonoidHom.ker (decompositionGroupResidueAction (K := K) A) =
      inertiaGroup K A

theorem

decompositionGroupResidueAction_surjective

L358 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction_surjective

Documentation

The residue-action exact sequence, including the infinite case: reduction is onto the full residue Galois group.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

theorem decompositionGroupResidueAction_surjective
    (A : _root_.ValuationSubring L) :
    Function.Surjective (decompositionGroupResidueAction (K := K) A)

instance

decompositionResidueExtension_normal

L395 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionResidueExtension_normal

Documentation

The residue-action exact sequence: λ/κ is normal, also in the infinite case.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

instance decompositionResidueExtension_normal
    (A : _root_.ValuationSubring L) :
    Normal (decompositionResidueField K A) (selectedResidueField A)

theorem

inertiaGroup_mulExact_decompositionGroupResidueAction

L417 ↗

RamificationTheory.HilbertRamification.ValuationSubring.inertiaGroup_mulExact_decompositionGroupResidueAction

Documentation

Exactness at G_w in the residue-action exact sequence.

Source context 9 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]
omit [IsGalois K L] in

Lean source · statement

theorem inertiaGroup_mulExact_decompositionGroupResidueAction
    (A : _root_.ValuationSubring L) :
    Function.MulExact (inertiaGroup K A).subtype
      (decompositionGroupResidueAction (K := K) A)

theorem

decompositionGroupResidueAction_shortExact

L426 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionGroupResidueAction_shortExact

Documentation

The residue-action exact sequence, arbitrary Galois form: 1 → I_w → G_w → Gal(λ/κ) → 1.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

theorem decompositionGroupResidueAction_shortExact
    (A : _root_.ValuationSubring L) :
    Function.Injective (inertiaGroup K A).subtype ∧
      Function.MulExact (inertiaGroup K A).subtype
        (decompositionGroupResidueAction (K := K) A) ∧
      Function.Surjective (decompositionGroupResidueAction (K := K) A)

def

decompositionQuotientEquivResidueGalois

L437 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionQuotientEquivResidueGalois

Documentation

Quotient form of the residue-action exact sequence.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

def decompositionQuotientEquivResidueGalois
    (A : _root_.ValuationSubring L) :
    decompositionGroup K A ⧸ inertiaGroup K A ≃*
      (selectedResidueField A ≃ₐ[decompositionResidueField K A]
        selectedResidueField A)

theorem

decompositionQuotientEquivResidueGalois_mk

L449 ↗

RamificationTheory.HilbertRamification.ValuationSubring.decompositionQuotientEquivResidueGalois_mk

Documentation

States the theorem decompositionQuotientEquivResidueGalois_mk.

Source context 8 commands

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

namespace RamificationTheory
noncomputable section
universe u v
namespace HilbertRamification
namespace ValuationSubring
open scoped Pointwise Topology
variable (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L]
variable [IsGalois K L]

Lean source · statement

theorem decompositionQuotientEquivResidueGalois_mk
    (A : _root_.ValuationSubring L) (sigma : decompositionGroup K A) :
    decompositionQuotientEquivResidueGalois (K := K) A
        (QuotientGroup.mk' (inertiaGroup K A) sigma) =
      decompositionGroupResidueAction (K := K) A sigma

Module documentation

The residue-action exact sequence

Declarations