NYLL
Module

RingInertiaCardinality.lean

Nyll.ValuedFieldTheory.Ramification.HilbertRamification.RingInertiaCardinality
2 declarations indexed from sourceView source ↗

Module documentation

Cardinality factorization for DVR inertia

Proves that the cardinality of inertia is the tame image order multiplied by the cardinality of principal-unit inertia.

Imports3
Imported by2

Declarations

theorem

card_eq_range_card_mul_ker_card

L22 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.card_eq_range_card_mul_ker_card
Source context 2 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
Lean source · statement
theorem card_eq_range_card_mul_ker_card
    {M : Type u} {N : Type v} [Group M] [Group N] (f : M →* N) :
    Nat.card M = Nat.card f.range * Nat.card f.ker
theorem

inertia_card_eq_tameOrder_mul_principalUnitInertia_card

L33 ↗
RamificationTheory.HilbertRamification.DiscreteValuationRing.inertia_card_eq_tameOrder_mul_principalUnitInertia_card
Documentation

The actual inertia order factors into the actual tame image order and the actual principal-unit kernel order, without exposing a second quotient type.

Source context 4 commands

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

namespace RamificationTheory.HilbertRamification.DiscreteValuationRing
universe u v
variable (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
variable (G : Type v) [Group G] [MulSemiringAction G R]
Lean source · statement
theorem inertia_card_eq_tameOrder_mul_principalUnitInertia_card :
    Nat.card ((IsLocalRing.maximalIdeal R).inertia G) =
      tameOrder R G * Nat.card (principalUnitInertia R G)

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