Ramification of infinite places of a number field #
This file studies the ramification of infinite places of a number field.
Main Definitions and Results #
NumberField.InfinitePlace.comap
: the restriction of an infinite place along an embedding.NumberField.InfinitePlace.orbitRelEquiv
: the equiv between the orbits of infinite places under the action of the galois group and the infinite places of the base field.NumberField.InfinitePlace.IsUnramified
: an infinite place is unramified in a field extension if the restriction has the same multiplicity.NumberField.InfinitePlace.not_isUnramified_iff
: an infinite place is not unramified (i.e., is ramified) iff it is a complex place above a real place.NumberField.InfinitePlace.IsUnramifiedIn
: an infinite place of the base field is unramified in a field extension if every infinite place over it is unramified.IsUnramifiedAtInfinitePlaces
: a field extension is unramified at infinite places if every infinite place is unramified.
Tags #
number field, infinite places, ramification
The restriction of an infinite place along an embedding.
Instances For
The action of the galois group on infinite places.
Equations
- NumberField.InfinitePlace.instMulActionAlgEquiv = { smul := fun (σ : K ≃ₐ[k] K) (w : NumberField.InfinitePlace K) => w.comap ↑σ.symm, one_smul := ⋯, mul_smul := ⋯ }
The orbits of infinite places under the action of the galois group are indexed by the infinite places of the base field.
Equations
- NumberField.InfinitePlace.orbitRelEquiv = Equiv.ofBijective (Quotient.lift (fun (x : NumberField.InfinitePlace K) => x.comap (algebraMap k K)) ⋯) ⋯
Instances For
An infinite place is unramified in a field extension if the restriction has the same multiplicity.
Equations
- NumberField.InfinitePlace.IsUnramified k w = ((w.comap (algebraMap k K)).mult = w.mult)
Instances For
An infinite place is ramified in a field extension if it is not unramified.
Equations
Instances For
An infinite place is not unramified (ie. ramified) iff it is a complex place above a real place.
A infinite place of the base field is unramified in a field extension if every infinite place over it is unramified.
Equations
- NumberField.InfinitePlace.IsUnramifiedIn K w = ∀ (v : NumberField.InfinitePlace K), v.comap (algebraMap k K) = w → NumberField.InfinitePlace.IsUnramified k v
Instances For
A field extension is unramified at infinite places if every infinite place is unramified.
- isUnramified (w : NumberField.InfinitePlace K) : NumberField.InfinitePlace.IsUnramified k w