Module

InertiaRestrictionCard.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.InertiaRestrictionCard

2 declarations indexed from sourceView source ↗

Module documentation

Cardinality under inertia scalar restriction

This is the finite-cardinality consequence of the inertia-subgroup cardinality formula used when the base completion is identified with a concrete local field.

Imports2

Mathlib.Algebra.Group.Subgroup.Finite
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.DecompositionGroup

Imported by2

theorem

inertiaGroupRestrictScalars_injective

L33 ↗

HilbertRamification.ValuationSubring.inertiaGroupRestrictScalars_injective

Documentation

Restriction of scalars embeds the inertia group over an intermediate base into the inertia group over the smaller base.

Source context 9 commands

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

noncomputable section
universe u v w
namespace HilbertRamification
namespace ValuationSubring
open RamificationTheory.HilbertRamification.ValuationSubring
variable {K : Type u} {M : Type v} {L : Type w}
variable [Field K] [Field M] [Field L]
variable [Algebra K M] [Algebra M L] [Algebra K L]
variable [IsScalarTower K M L]

Lean source · statement

theorem inertiaGroupRestrictScalars_injective
    (A : _root_.ValuationSubring L) :
    Function.Injective
      (inertiaGroupRestrictScalars (K := K) (M := M) A)

theorem

natCard_inertiaGroup_le_restrictScalars

L49 ↗

HilbertRamification.ValuationSubring.natCard_inertiaGroup_le_restrictScalars