Documentation

Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification

Ramification of infinite places of a number field #

This file studies the ramification of infinite places of a number field.

Main Definitions and Results #

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.

Equations
Instances For
    @[simp]
    theorem NumberField.InfinitePlace.comap_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] (φ : K →+* ) (f : k →+* K) :
    (mk φ).comap f = mk (φ.comp f)
    theorem NumberField.InfinitePlace.comap_comp {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] (w : InfinitePlace K) (f : F →+* K) (g : k →+* F) :
    w.comap (f.comp g) = (w.comap f).comap g
    theorem NumberField.InfinitePlace.IsReal.comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) {w : InfinitePlace K} ( : w.IsReal) :
    theorem NumberField.InfinitePlace.isReal_comap_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k ≃+* K) {w : InfinitePlace K} :
    (w.comap f).IsReal w.IsReal
    theorem NumberField.InfinitePlace.mult_comap_le {k : Type u_1} [Field k] {K : Type u_2} [Field K] (f : k →+* K) (w : InfinitePlace K) :
    (w.comap f).mult w.mult

    The action of the galois group on infinite places.

    Equations
    @[simp]
    theorem NumberField.InfinitePlace.instMulActionAlgEquiv_smul_coe_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) (a✝ : K) :
    (SMul.smul σ w) a✝ = w (σ.symm a✝)
    theorem NumberField.InfinitePlace.smul_eq_comap {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) :
    σ w = w.comap σ.symm
    @[simp]
    theorem NumberField.InfinitePlace.smul_apply {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) (x : K) :
    (σ w) x = w (σ.symm x)
    @[simp]
    theorem NumberField.InfinitePlace.smul_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (σ : K ≃ₐ[k] K) (φ : K →+* ) :
    σ mk φ = mk (φ.comp σ.symm)
    theorem NumberField.InfinitePlace.comap_smul {k : Type u_1} [Field k] {K : Type u_2} [Field K] {F : Type u_3} [Field F] [Algebra k K] (σ : K ≃ₐ[k] K) (w : InfinitePlace K) {f : F →+* K} :
    (σ w).comap f = w.comap ((↑σ.symm).comp f)
    theorem NumberField.InfinitePlace.isReal_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : InfinitePlace K} :
    (σ w).IsReal w.IsReal
    theorem NumberField.InfinitePlace.isComplex_smul_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {w : InfinitePlace K} :
    theorem NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] (φ ψ : K →+* ) (h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)) :
    ∃ (σ : K ≃ₐ[k] K), φ.comp σ.symm = ψ
    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)) :
    ∃ (σ : K ≃ₐ[k] K), σ w = w'
    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} :

    The orbits of infinite places under the action of the galois group are indexed by the infinite places of the base field.

    Equations
    Instances For
      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
      Instances For
        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) :
        (w.comap (algebraMap k K)).mult = w.mult
        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) :
        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) :

        An infinite place is not unramified (ie. ramified) iff it is a complex place above a real place.

        theorem NumberField.InfinitePlace.isUnramified_mk_iff_forall_isConj {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] [IsGalois k K] {φ : K →+* } :
        IsUnramified k (mk φ) ∀ (σ : K ≃ₐ[k] K), ComplexEmbedding.IsConj φ σσ = 1
        theorem NumberField.InfinitePlace.mem_stabilizer_mk_iff {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] (φ : K →+* ) (σ : K ≃ₐ[k] K) :
        theorem NumberField.ComplexEmbedding.IsConj.coe_stabilzer_mk {k : Type u_1} [Field k] {K : Type u_2} [Field K] [Algebra k K] {σ : K ≃ₐ[k] K} {φ : K →+* } (h : IsConj φ σ) :
        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} :

        A infinite place of the base field is unramified in a field extension if every infinite place over it is unramified.

        Equations
        Instances For
          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.

          Instances