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
def
NumberField.InfinitePlace.comap
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
(w : InfinitePlace K)
(f : k →+* K)
:
The restriction of an infinite place along an embedding.
Instances For
theorem
NumberField.InfinitePlace.comap_mk_lift
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[Algebra.IsAlgebraic k K]
(φ : k →+* ℂ)
:
theorem
NumberField.InfinitePlace.comap_surjective
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[Algebra.IsAlgebraic k K]
:
Function.Surjective fun (x : InfinitePlace K) => x.comap (algebraMap k K)
theorem
NumberField.InfinitePlace.card_mono
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
[NumberField k]
[NumberField K]
:
instance
NumberField.InfinitePlace.instMulActionAlgEquiv
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
:
MulAction (K ≃ₐ[k] K) (InfinitePlace K)
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 := ⋯ }
theorem
NumberField.InfinitePlace.exists_smul_eq_of_comap_eq
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
{w w' : InfinitePlace K}
(h : w.comap (algebraMap k K) = w'.comap (algebraMap k K))
:
theorem
NumberField.InfinitePlace.mem_orbit_iff
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
{w w' : InfinitePlace K}
:
noncomputable def
NumberField.InfinitePlace.orbitRelEquiv
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
:
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
theorem
NumberField.InfinitePlace.orbitRelEquiv_apply_mk''
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
(w : InfinitePlace K)
:
def
NumberField.InfinitePlace.IsUnramified
(k : Type u_1)
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
(w : InfinitePlace K)
:
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
theorem
NumberField.InfinitePlace.isUnramified_self
{K : Type u_2}
[Field K]
(w : InfinitePlace K)
:
IsUnramified K w
theorem
NumberField.InfinitePlace.IsUnramified.eq
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
(h : IsUnramified k w)
:
theorem
NumberField.InfinitePlace.isUnramified_iff_mult_le
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
:
theorem
NumberField.InfinitePlace.IsUnramified.comap_algHom
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
{F : Type u_3}
[Field F]
[Algebra k K]
[Algebra k F]
{w : InfinitePlace F}
(h : IsUnramified k w)
(f : K →ₐ[k] F)
:
IsUnramified k (w.comap ↑f)
theorem
NumberField.InfinitePlace.IsUnramified.of_restrictScalars
{k : Type u_1}
[Field k]
(K : Type u_2)
[Field K]
{F : Type u_3}
[Field F]
[Algebra k K]
[Algebra k F]
[Algebra K F]
[IsScalarTower k K F]
{w : InfinitePlace F}
(h : IsUnramified k w)
:
IsUnramified K w
theorem
NumberField.InfinitePlace.IsUnramified.comap
{k : Type u_1}
[Field k]
(K : Type u_2)
[Field K]
{F : Type u_3}
[Field F]
[Algebra k K]
[Algebra k F]
[Algebra K F]
[IsScalarTower k K F]
{w : InfinitePlace F}
(h : IsUnramified k w)
:
IsUnramified k (w.comap (algebraMap K F))
theorem
NumberField.InfinitePlace.not_isUnramified_iff
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
:
An infinite place is not unramified (ie. ramified) iff it is a complex place above a real place.
theorem
NumberField.InfinitePlace.isUnramified_iff
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
:
theorem
NumberField.InfinitePlace.IsReal.isUnramified
(k : Type u_1)
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
(h : w.IsReal)
:
IsUnramified k w
theorem
NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
(h : IsUnramified k w)
:
theorem
NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two
(k : Type u_1)
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
(w : InfinitePlace K)
:
theorem
NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
[IsGalois k K]
:
theorem
NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
[IsGalois k K]
:
theorem
NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
[IsGalois k K]
:
theorem
NumberField.InfinitePlace.card_stabilizer
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
[IsGalois k K]
:
theorem
NumberField.InfinitePlace.even_nat_card_aut_of_not_isUnramified
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
[IsGalois k K]
(hw : ¬IsUnramified k w)
:
theorem
NumberField.InfinitePlace.even_card_aut_of_not_isUnramified
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
[IsGalois k K]
[FiniteDimensional k K]
(hw : ¬IsUnramified k w)
:
Even (Fintype.card (K ≃ₐ[k] K))
theorem
NumberField.InfinitePlace.even_finrank_of_not_isUnramified
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{w : InfinitePlace K}
[IsGalois k K]
(hw : ¬IsUnramified k w)
:
Even (Module.finrank k K)
theorem
NumberField.InfinitePlace.isUnramified_smul_iff
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
{σ : K ≃ₐ[k] K}
{w : InfinitePlace K}
:
def
NumberField.InfinitePlace.IsUnramifiedIn
{k : Type u_1}
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
(w : InfinitePlace k)
:
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
theorem
NumberField.InfinitePlace.isUnramifiedIn_comap
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
{w : InfinitePlace K}
:
theorem
NumberField.InfinitePlace.even_card_aut_of_not_isUnramifiedIn
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
[FiniteDimensional k K]
{w : InfinitePlace k}
(hw : ¬IsUnramifiedIn K w)
:
Even (Fintype.card (K ≃ₐ[k] K))
theorem
NumberField.InfinitePlace.even_finrank_of_not_isUnramifiedIn
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
{w : InfinitePlace k}
(hw : ¬IsUnramifiedIn K w)
:
Even (Module.finrank k K)
theorem
NumberField.InfinitePlace.card_isUnramified
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
[NumberField K]
[NumberField k]
[IsGalois k K]
:
{w : InfinitePlace K | IsUnramified k w}.card = {w : InfinitePlace k | IsUnramifiedIn K w}.card * Module.finrank k K
theorem
NumberField.InfinitePlace.card_isUnramified_compl
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
[NumberField K]
[NumberField k]
[IsGalois k K]
:
{w : InfinitePlace K | IsUnramified k w}ᶜ.card = {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ.card * (Module.finrank k K / 2)
theorem
NumberField.InfinitePlace.card_eq_card_isUnramifiedIn
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
[NumberField K]
[NumberField k]
[IsGalois k K]
:
Fintype.card (InfinitePlace K) = {w : InfinitePlace k | IsUnramifiedIn K w}.card * Module.finrank k K + {w : InfinitePlace k | IsUnramifiedIn K w}ᶜ.card * (Module.finrank k K / 2)
class
IsUnramifiedAtInfinitePlaces
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
:
A field extension is unramified at infinite places if every infinite place is unramified.
- isUnramified (w : NumberField.InfinitePlace K) : NumberField.InfinitePlace.IsUnramified k w
Instances
theorem
IsUnramifiedAtInfinitePlaces.trans
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
(F : Type u_3)
[Field F]
[Algebra k K]
[Algebra k F]
[Algebra K F]
[IsScalarTower k K F]
[h₁ : IsUnramifiedAtInfinitePlaces k K]
[h₂ : IsUnramifiedAtInfinitePlaces K F]
:
theorem
IsUnramifiedAtInfinitePlaces.top
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
(F : Type u_3)
[Field F]
[Algebra k K]
[Algebra k F]
[Algebra K F]
[IsScalarTower k K F]
[h : IsUnramifiedAtInfinitePlaces k F]
:
theorem
IsUnramifiedAtInfinitePlaces.bot
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
(F : Type u_3)
[Field F]
[Algebra k K]
[Algebra k F]
[Algebra K F]
[IsScalarTower k K F]
[h₁ : IsUnramifiedAtInfinitePlaces k F]
[Algebra.IsAlgebraic K F]
:
theorem
NumberField.InfinitePlace.isUnramified
(k : Type u_1)
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsUnramifiedAtInfinitePlaces k K]
(w : InfinitePlace K)
:
IsUnramified k w
theorem
NumberField.InfinitePlace.isUnramifiedIn
{k : Type u_1}
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
[IsUnramifiedAtInfinitePlaces k K]
(w : InfinitePlace k)
:
IsUnramifiedIn K w
theorem
IsUnramifiedAtInfinitePlaces_of_odd_card_aut
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
[FiniteDimensional k K]
(h : Odd (Fintype.card (K ≃ₐ[k] K)))
:
theorem
IsUnramifiedAtInfinitePlaces_of_odd_finrank
{k : Type u_1}
[Field k]
{K : Type u_2}
[Field K]
[Algebra k K]
[IsGalois k K]
(h : Odd (Module.finrank k K))
:
theorem
IsUnramifiedAtInfinitePlaces.card_infinitePlace
(k : Type u_1)
[Field k]
(K : Type u_2)
[Field K]
[Algebra k K]
[NumberField k]
[NumberField K]
[IsGalois k K]
[IsUnramifiedAtInfinitePlaces k K]
: