Documentation

Iwasawalib.NumberTheory.NumberField.HilbertClassField.Basic

Hilbert class field (experimental) - basic definitions #

Assertion that a field extension is unramified outside S #

source
class NumberField.IsUnramifiedOutside (F : Type u_3) (K : Type u_4) (L : Type u_5) [Field F] [Field K] [Field L] [Algebra F K] [Algebra L K] [Algebra.IsAlgebraic F K] (S : Set (AbsoluteValue L ℝ)) :
Prop

A typeclass asserting that an algebraic extension K / F is unramified outside S, where S is a set of places of a subfield L of K.

Instances
    source
    theorem NumberField.isUnramifiedOutside_iff (F : Type u_3) (K : Type u_4) (L : Type u_5) [Field F] [Field K] [Field L] [Algebra F K] [Algebra L K] [Algebra.IsAlgebraic F K] (S : Set (AbsoluteValue L ℝ)) :
    IsUnramifiedOutside F K L S ↔ ∀ (v : AbsoluteValue L ℝ), v.IsNontrivial → (∀ w ∈ S, ¬v ≈ w) → AbsoluteValue.IsUnramifiedIn F K v
    source
    theorem NumberField.isUnramifiedOutside_of_isUnramifiedOutside_preimage (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] (L : Type u_3) (L' : Type u_4) [Field L] [Field L'] [Algebra L K] [Algebra L' L] [Algebra L' K] [IsScalarTower L' L K] (S : Set (AbsoluteValue L' ℝ)) [H : IsUnramifiedOutside F K L ((fun (x : AbsoluteValue L ℝ) => x.comp ⋯) ⁻¹' S)] :
    IsUnramifiedOutside F K L' S
    source
    theorem NumberField.isUnramifiedOutside_preimage_iff (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] (L : Type u_3) (L' : Type u_4) [Field L] [Field L'] [Algebra L K] [Algebra L' L] [Algebra.IsAlgebraic L' L] [Algebra L' K] [IsScalarTower L' L K] (S : Set (AbsoluteValue L' ℝ)) :
    IsUnramifiedOutside F K L ((fun (x : AbsoluteValue L ℝ) => x.comp ⋯) ⁻¹' S) ↔ IsUnramifiedOutside F K L' S
    source
    @[reducible, inline]
    abbrev NumberField.IsUnramifiedEverywhere (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] :
    Prop

    A typeclass asserting that an algebraic extension K / F is unramified everywhere.

    Equations
    Instances For
      source
      theorem NumberField.isUnramifiedEverywhere_iff (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] [Algebra.IsAlgebraic F K] :
      IsUnramifiedEverywhere F K ↔ ∀ (v : AbsoluteValue K ℝ), v.IsNontrivial → AbsoluteValue.IsUnramified F v
      source
      theorem NumberField.isUnramifiedOutside_empty_iff (F : Type u_3) (K : Type u_4) (L : Type u_5) [Field F] [Field K] [Field L] [Algebra F K] [Algebra L K] [Algebra.IsAlgebraic F K] [Algebra.IsAlgebraic L K] :
      IsUnramifiedOutside F K L ∅ ↔ IsUnramifiedEverywhere F K
      source
      @[instance 100]
      instance NumberField.isUnramifiedOutside_empty_of_isUnramifiedEverywhere (F : Type u_3) (K : Type u_4) (L : Type u_5) [Field F] [Field K] [Field L] [Algebra F K] [Algebra L K] [Algebra.IsAlgebraic F K] [Algebra.IsAlgebraic L K] [IsUnramifiedEverywhere F K] :
      IsUnramifiedOutside F K L ∅
      source
      theorem NumberField.IsUnramifiedOutside.tower_top (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] (L : Type u_4) [Field L] [Algebra L M] (S : Set (AbsoluteValue L ℝ)) [Algebra.IsAlgebraic F M] [IsUnramifiedOutside F M L S] :
      IsUnramifiedOutside K M L S
      source
      theorem NumberField.IsUnramifiedOutside.tower_bot (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] (L : Type u_4) [Field L] [Algebra L K] [Algebra L M] [IsScalarTower L K M] (S : Set (AbsoluteValue L ℝ)) [Algebra.IsAlgebraic F M] [IsUnramifiedOutside F M L S] :
      IsUnramifiedOutside F K L S
      source
      theorem NumberField.IsUnramifiedOutside.trans (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] (L : Type u_4) [Field L] [Algebra L K] [Algebra L M] [IsScalarTower L K M] (S : Set (AbsoluteValue L ℝ)) [Algebra.IsAlgebraic F K] [IsUnramifiedOutside F K L S] [Algebra.IsAlgebraic K M] [IsUnramifiedOutside K M L S] :
      IsUnramifiedOutside F M L S
      source
      theorem NumberField.IsUnramifiedEverywhere.tower_top (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [Algebra.IsAlgebraic F M] [IsUnramifiedEverywhere F M] :
      IsUnramifiedEverywhere K M
      source
      theorem NumberField.IsUnramifiedEverywhere.tower_bot (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [Algebra.IsAlgebraic F M] [IsUnramifiedEverywhere F M] :
      IsUnramifiedEverywhere F K
      source
      theorem NumberField.IsUnramifiedEverywhere.trans (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [Algebra.IsAlgebraic F K] [IsUnramifiedEverywhere F K] [Algebra.IsAlgebraic K M] [IsUnramifiedEverywhere K M] :
      IsUnramifiedEverywhere F M

      Maximal unramified algebra subextension #

      source
      def NumberField.maximalExtensionUnramifiedOutside (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) :
      IntermediateField F K

      The maximal algebra subextension of K / F unramified outside S, where S is a set of places of a subfield L of F.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[reducible, inline]
        abbrev NumberField.maximalUnramifiedExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] :
        IntermediateField F K

        The maximal unramified algebra subextension of K / F.

        Equations
        Instances For
          source
          instance NumberField.isAlgebraic_maximalExtensionUnramifiedOutside (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) :
          Algebra.IsAlgebraic F ↥(maximalExtensionUnramifiedOutside F K L S)
          source
          instance NumberField.isUnramifiedOutside_maximalExtensionUnramifiedOutside (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) :
          IsUnramifiedOutside F (↥(maximalExtensionUnramifiedOutside F K L S)) F ((fun (x : AbsoluteValue F ℝ) => x.comp ⋯) ⁻¹' S)
          source
          instance NumberField.isUnramifiedOutside_maximalExtensionUnramifiedOutside' (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] [Algebra L K] [IsScalarTower L F K] (S : Set (AbsoluteValue L ℝ)) :
          IsUnramifiedOutside F (↥(maximalExtensionUnramifiedOutside F K L S)) L S
          source
          instance NumberField.isUnramifiedEverywhere_maximalUnramifiedExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] :
          IsUnramifiedEverywhere F ↥(maximalUnramifiedExtension F K)
          source
          theorem NumberField.le_maximalExtensionUnramifiedOutside (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) (E : IntermediateField F K) [Algebra.IsAlgebraic F ↥E] [IsUnramifiedOutside F (↥E) F ((fun (x : AbsoluteValue F ℝ) => x.comp ⋯) ⁻¹' S)] :
          E ≤ maximalExtensionUnramifiedOutside F K L S
          source
          theorem NumberField.le_maximalExtensionUnramifiedOutside_iff (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) (E : IntermediateField F K) :
          E ≤ maximalExtensionUnramifiedOutside F K L S ↔ ∃ (x : Algebra.IsAlgebraic F ↥E), IsUnramifiedOutside F (↥E) F ((fun (x : AbsoluteValue F ℝ) => x.comp ⋯) ⁻¹' S)
          source
          theorem NumberField.le_maximalExtensionUnramifiedOutside' (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] [Algebra.IsAlgebraic L F] [Algebra L K] [IsScalarTower L F K] (S : Set (AbsoluteValue L ℝ)) (E : IntermediateField F K) [Algebra.IsAlgebraic F ↥E] [IsUnramifiedOutside F (↥E) L S] :
          E ≤ maximalExtensionUnramifiedOutside F K L S
          source
          theorem NumberField.le_maximalExtensionUnramifiedOutside_iff' (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] [Algebra.IsAlgebraic L F] [Algebra L K] [IsScalarTower L F K] (S : Set (AbsoluteValue L ℝ)) (E : IntermediateField F K) :
          E ≤ maximalExtensionUnramifiedOutside F K L S ↔ ∃ (x : Algebra.IsAlgebraic F ↥E), IsUnramifiedOutside F (↥E) L S
          source
          theorem NumberField.le_maximalUnramifiedExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E : IntermediateField F K) [Algebra.IsAlgebraic F ↥E] [IsUnramifiedEverywhere F ↥E] :
          E ≤ maximalUnramifiedExtension F K
          source
          theorem NumberField.le_maximalUnramifiedExtension_iff (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E : IntermediateField F K) :
          E ≤ maximalUnramifiedExtension F K ↔ ∃ (x : Algebra.IsAlgebraic F ↥E), IsUnramifiedEverywhere F ↥E
          source
          theorem NumberField.isGalois_maximalExtensionUnramifiedOutside_of_isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [IsGalois F M] [IsGalois F K] (L : Type u_4) [Field L] [Algebra L F] [Algebra L K] [IsScalarTower L F K] (S : Set (AbsoluteValue L ℝ)) :
          IsGalois F ↥(maximalExtensionUnramifiedOutside K M L S)

          Suppose M / K / F is a field extension tower, such that M / F and K / F are Galois. Let H / K be the maximal algebra subextension of M / K unramified outside S, where S is a set of places of a subfield L of F. Then H / F is also Galois.

          source
          theorem NumberField.isGalois_maximalUnramifiedExtension_of_isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [IsGalois F M] [IsGalois F K] :
          IsGalois F ↥(maximalUnramifiedExtension K M)

          Suppose M / K / F is a field extension tower, such that M / F and K / F are Galois. Let H / K be the maximal unramified algebra subextension of M / K. Then H / F is also Galois.

          Maximal unramified abelian subextension #

          source
          def NumberField.maximalAbelianExtensionUnramifiedOutside (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) :
          IntermediateField F K

          The maximal abelian subextension of K / F unramified outside S, where S is a set of places of a subfield L of F, is defined to be the maximal abelian subextension of the maximal algebraic subextension of K / F unramified outside S.

          Equations
          Instances For
            source
            @[reducible, inline]
            abbrev NumberField.maximalUnramifiedAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] :
            IntermediateField F K

            The maximal unramified abelian subextension of K / F, is defined to be the maximal abelian subextension of the maximal unramified algebraic subextension of K / F.

            Equations
            Instances For
              source
              instance NumberField.isAbelianGalois_maximalAbelianExtensionUnramifiedOutside (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) :
              IsAbelianGalois F ↥(maximalAbelianExtensionUnramifiedOutside F K L S)
              source
              instance NumberField.isUnramifiedOutside_maximalAbelianExtensionUnramifiedOutside (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) :
              IsUnramifiedOutside F (↥(maximalAbelianExtensionUnramifiedOutside F K L S)) F ((fun (x : AbsoluteValue F ℝ) => x.comp ⋯) ⁻¹' S)
              source
              instance NumberField.isUnramifiedOutside_maximalAbelianExtensionUnramifiedOutside' (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] [Algebra L K] [IsScalarTower L F K] (S : Set (AbsoluteValue L ℝ)) :
              IsUnramifiedOutside F (↥(maximalAbelianExtensionUnramifiedOutside F K L S)) L S
              source
              instance NumberField.isUnramifiedEverywhere_maximalUnramifiedAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] :
              IsUnramifiedEverywhere F ↥(maximalUnramifiedAbelianExtension F K)
              source
              theorem NumberField.le_maximalAbelianExtensionUnramifiedOutside (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) (E : IntermediateField F K) [IsAbelianGalois F ↥E] [IsUnramifiedOutside F (↥E) F ((fun (x : AbsoluteValue F ℝ) => x.comp ⋯) ⁻¹' S)] :
              E ≤ maximalAbelianExtensionUnramifiedOutside F K L S
              source
              theorem NumberField.le_maximalAbelianExtensionUnramifiedOutside_iff (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] (S : Set (AbsoluteValue L ℝ)) (E : IntermediateField F K) :
              E ≤ maximalAbelianExtensionUnramifiedOutside F K L S ↔ ∃ (x : IsAbelianGalois F ↥E), IsUnramifiedOutside F (↥E) F ((fun (x : AbsoluteValue F ℝ) => x.comp ⋯) ⁻¹' S)
              source
              theorem NumberField.le_maximalAbelianExtensionUnramifiedOutside' (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] [Algebra.IsAlgebraic L F] [Algebra L K] [IsScalarTower L F K] (S : Set (AbsoluteValue L ℝ)) (E : IntermediateField F K) [IsAbelianGalois F ↥E] [IsUnramifiedOutside F (↥E) L S] :
              E ≤ maximalAbelianExtensionUnramifiedOutside F K L S
              source
              theorem NumberField.le_maximalAbelianExtensionUnramifiedOutside_iff' (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (L : Type u_3) [Field L] [Algebra L F] [Algebra.IsAlgebraic L F] [Algebra L K] [IsScalarTower L F K] (S : Set (AbsoluteValue L ℝ)) (E : IntermediateField F K) :
              E ≤ maximalAbelianExtensionUnramifiedOutside F K L S ↔ ∃ (x : IsAbelianGalois F ↥E), IsUnramifiedOutside F (↥E) L S
              source
              theorem NumberField.le_maximalUnramifiedAbelianExtension (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E : IntermediateField F K) [IsAbelianGalois F ↥E] [IsUnramifiedEverywhere F ↥E] :
              E ≤ maximalUnramifiedAbelianExtension F K
              source
              theorem NumberField.le_maximalUnramifiedAbelianExtension_iff (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (E : IntermediateField F K) :
              E ≤ maximalUnramifiedAbelianExtension F K ↔ ∃ (x : IsAbelianGalois F ↥E), IsUnramifiedEverywhere F ↥E
              source
              theorem NumberField.isGalois_maximalAbelianExtensionUnramifiedOutside_of_isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [IsGalois F M] [IsGalois F K] (L : Type u_4) [Field L] [Algebra L F] [Algebra L K] [IsScalarTower L F K] (S : Set (AbsoluteValue L ℝ)) :
              IsGalois F ↥(maximalAbelianExtensionUnramifiedOutside K M L S)

              Suppose M / K / F is a field extension tower, such that M / F and K / F are Galois. Let H / K be the maximal abelian subextension of M / K unramified outside S, where S is a set of places of a subfield L of F. Then H / F is also Galois.

              source
              theorem NumberField.isGalois_maximalUnramifiedAbelianExtension_of_isGalois (F : Type u_1) (K : Type u_2) [Field F] [Field K] [Algebra F K] (M : Type u_3) [Field M] [Algebra F M] [Algebra K M] [IsScalarTower F K M] [IsGalois F M] [IsGalois F K] :
              IsGalois F ↥(maximalUnramifiedAbelianExtension K M)

              Suppose M / K / F is a field extension tower, such that M / F and K / F are Galois. Let H / K be the maximal unramified abelian subextension of M / K. Then H / F is also Galois.