Module

PrimesOver.lean

Nyll.SchemeTheory.FunctionFields.PrimeDivisors.PrimesOver

2 declarations indexed from sourceView source ↗

Module documentation

Counting primes above a prime ideal

The fundamental equality between ramification indices, inertia degrees, and the rank of a finite flat extension immediately bounds the number of primes above a fixed prime. This file records that consequence in a form convenient for the prime-divisor counts in Fried--Jarden, Lemma 6.2.2.

Imports1

Mathlib.RingTheory.RamificationInertia.Basic

Imported by2

theorem

card_primesOver_le_finrank

L37 ↗

FieldArithmetic.Chapter06.PrimeCounting.card_primesOver_le_finrank

Documentation

The number of primes of a finite flat algebra above a prime ideal is at most the rank of the algebra.

This is slightly stronger than the Dedekind-domain version needed for function fields: every ramification-index/inertia-degree summand is positive, so the number of summands is bounded by their sum.

Source context 7 commands

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

noncomputable section
namespace FieldArithmetic
namespace Chapter06
namespace PrimeCounting
universe u v
variable {R : Type u} {S : Type v}
variable [CommRing R] [CommRing S] [Algebra R S]

Lean source · statement

theorem card_primesOver_le_finrank
    [IsDomain R] [Module.Finite R S] [Module.Flat R S]
    (p : Ideal R) [p.IsPrime] :
    Nat.card (p.primesOver S) ≤ Module.finrank R S

theorem

card_primesOver_le_finrank_of_isDedekindDomain

L57 ↗

FieldArithmetic.Chapter06.PrimeCounting.card_primesOver_le_finrank_of_isDedekindDomain