Documentation

Mathlib.FieldTheory.KrullTopology

Krull topology #

We define the Krull topology on L ≃ₐ[K] L for an arbitrary field extension L/K. In order to do this, we first define a GroupFilterBasis on L ≃ₐ[K] L, whose sets are E.fixingSubgroup for all intermediate fields E with E/K finite dimensional.

Main Definitions #

Main Results #

Notations #

Implementation Notes #

theorem IntermediateField.map_id {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) :

Mapping intermediate fields along the identity does not change them

instance im_finiteDimensional {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E : IntermediateField K L} (σ : L ≃ₐ[K] L) [FiniteDimensional K E] :

Mapping a finite dimensional intermediate field along an algebra equivalence gives a finite-dimensional intermediate field.

Equations
  • =
def finiteExts (K : Type u_1) [Field K] (L : Type u_2) [Field L] [Algebra K L] :

Given a field extension L/K, finiteExts K L is the set of intermediate field extensions L/E/K such that E/K is finite

Equations
Instances For
    def fixedByFinite (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :

    Given a field extension L/K, fixedByFinite K L is the set of subsets Gal(L/E) of L ≃ₐ[K] L, where E/K is finite

    Equations
    Instances For

      For a field extension L/K, the intermediate field K is finite-dimensional over K

      theorem IntermediateField.fixingSubgroup.bot {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] :
      .fixingSubgroup =

      This lemma says that Gal(L/K) = L ≃ₐ[K] L

      theorem top_fixedByFinite {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] :

      If L/K is a field extension, then we have Gal(L/K) ∈ fixedByFinite K L

      theorem finiteDimensional_sup {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E1 : IntermediateField K L) (E2 : IntermediateField K L) :
      FiniteDimensional K E1FiniteDimensional K E2FiniteDimensional K (E1 E2)

      If E1 and E2 are finite-dimensional intermediate fields, then so is their compositum. This rephrases a result already in mathlib so that it is compatible with our type classes

      theorem IntermediateField.mem_fixingSubgroup_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) (σ : L ≃ₐ[K] L) :
      σ E.fixingSubgroup xE, σ x = x

      An element of L ≃ₐ[K] L is in Gal(L/E) if and only if it fixes every element of E

      theorem IntermediateField.fixingSubgroup.antimono {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] {E1 : IntermediateField K L} {E2 : IntermediateField K L} (h12 : E1 E2) :
      E2.fixingSubgroup E1.fixingSubgroup

      The map E ↦ Gal(L/E) is inclusion-reversing

      def galBasis (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :

      Given a field extension L/K, galBasis K L is the filter basis on L ≃ₐ[K] L whose sets are Gal(L/E) for intermediate fields E with E/K finite dimensional

      Equations
      Instances For
        theorem mem_galBasis_iff (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] (U : Set (L ≃ₐ[K] L)) :
        U galBasis K L U (fun (g : Subgroup (L ≃ₐ[K] L)) => g.carrier) '' fixedByFinite K L

        A subset of L ≃ₐ[K] L is a member of galBasis K L if and only if it is the underlying set of Gal(L/E) for some finite subextension E/K

        def galGroupBasis (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :

        For a field extension L/K, galGroupBasis K L is the group filter basis on L ≃ₐ[K] L whose sets are Gal(L/E) for finite subextensions E/K

        Equations
        Instances For
          instance krullTopology (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :

          For a field extension L/K, krullTopology K L is the topological space structure on L ≃ₐ[K] L induced by the group filter basis galGroupBasis K L

          Equations
          instance instTopologicalGroupAlgEquiv (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :

          For a field extension L/K, the Krull topology on L ≃ₐ[K] L makes it a topological group.

          Equations
          • =
          theorem IntermediateField.fixingSubgroup_isOpen {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [FiniteDimensional K E] :
          IsOpen E.fixingSubgroup

          Let L/E/K be a tower of fields with E/K finite. Then Gal(L/E) is an open subgroup of L ≃ₐ[K] L.

          theorem IntermediateField.fixingSubgroup_isClosed {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (E : IntermediateField K L) [FiniteDimensional K E] :
          IsClosed E.fixingSubgroup

          Given a tower of fields L/E/K, with E/K finite, the subgroup Gal(L/E) ≤ L ≃ₐ[K] L is closed.

          theorem krullTopology_t2 {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] :

          If L/K is an algebraic extension, then the Krull topology on L ≃ₐ[K] L is Hausdorff.

          theorem krullTopology_totallyDisconnected {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [Algebra.IsIntegral K L] :

          If L/K is an algebraic field extension, then the Krull topology on L ≃ₐ[K] L is totally disconnected.

          @[simp]
          theorem IntermediateField.fixingSubgroup_top (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :
          .fixingSubgroup =
          @[simp]
          theorem IntermediateField.fixingSubgroup_bot (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] :
          .fixingSubgroup =