Documentation

TauCeti.FieldTheory.Galois.AbsoluteGaloisGroup.Congr

Absolute Galois groups of isomorphic fields #

A field isomorphism identifies separable closures and hence, contravariantly, their absolute Galois groups. This file packages that identification as an isomorphism of topological groups. It is useful when a field is presented through a canonical completion or another isomorphic model, while Galois-cohomological constructions are available on the standard model.

These equivalences underlie the transport of cohomological Brauer groups along field isomorphisms in TauCeti.NumberTheory.ClassFieldTheory.Brauer.Congr.

Subextensions of the chosen separable closures are transported by IntermediateField.separableClosureCongr. This preserves degree, finiteness and normality. The induced automorphism equivalence commutes with restriction from the absolute Galois groups and identifies the corresponding fixing subgroups.

Main definitions #

source
noncomputable def RingEquiv.separableClosureCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) :
SeparableClosure L ≃+* SeparableClosure K

A field isomorphism induces a chosen ring equivalence of separable closures.

Instances For
    source
    @[simp]
    theorem RingEquiv.separableClosureCongr_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (y : L) :
    e.separableClosureCongr ((algebraMap L (SeparableClosure L)) y) = (algebraMap K (SeparableClosure K)) (e.symm y)

    The chosen equivalence of separable closures extends e.symm.

    source
    @[simp]
    theorem RingEquiv.separableClosureCongr_symm_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (x : K) :
    e.separableClosureCongr.symm ((algebraMap K (SeparableClosure K)) x) = (algebraMap L (SeparableClosure L)) (e x)

    The inverse of the chosen equivalence of separable closures extends e.

    source
    noncomputable def RingEquiv.absoluteGaloisGroupCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) :
    TauCeti.AbsoluteGaloisGroup L ≃ₜ* TauCeti.AbsoluteGaloisGroup K

    A field isomorphism K ≃+* L induces a contravariant continuous equivalence G_L ≃ₜ* G_K of absolute Galois groups.

    Instances For
      source
      @[simp]
      theorem RingEquiv.absoluteGaloisGroupCongr_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (g : TauCeti.AbsoluteGaloisGroup L) (x : SeparableClosure K) :
      (e.absoluteGaloisGroupCongr g) x = e.separableClosureCongr (g (e.separableClosureCongr.symm x))

      The absolute-Galois-group equivalence induced by a field isomorphism acts by conjugation through the chosen equivalence of separable closures.

      source
      @[simp]
      theorem RingEquiv.absoluteGaloisGroupCongr_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (g : TauCeti.AbsoluteGaloisGroup K) (x : SeparableClosure L) :
      (e.absoluteGaloisGroupCongr.symm g) x = e.separableClosureCongr.symm (g (e.separableClosureCongr x))

      The inverse of the absolute-Galois-group equivalence induced by a field isomorphism acts by conjugation through the inverse of the chosen equivalence of separable closures.

      source
      theorem RingEquiv.restrictNormalHom_congr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) (E : IntermediateField K (SeparableClosure K)) [Normal K ↥E] (F : IntermediateField L (SeparableClosure L)) [Normal L ↥F] (ι : ↥E →+* ↥F) (π : Gal(↥F/L) →* Gal(↥E/K)) (hι : ∀ (x : ↥E), e.separableClosureCongr.symm (E.val x) = F.val (ι x)) (hπ : ∀ (g : Gal(↥F/L)) (x : ↥E), ι ((π g) x) = g (ι x)) (g : TauCeti.AbsoluteGaloisGroup L) :
      π ((AlgEquiv.restrictNormalHom ↥F) g) = (AlgEquiv.restrictNormalHom ↥E) (e.absoluteGaloisGroupCongr g)

      Restriction to identified normal subextensions commutes with field transport. The coefficient embedding identifies the subextensions inside the chosen separable closures.

      source
      noncomputable def IntermediateField.separableClosureCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) :
      IntermediateField L (SeparableClosure L)

      Transport a subextension through the chosen identification of separable closures.

      Instances For
        source
        @[simp]
        theorem IntermediateField.mem_separableClosureCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) (x : SeparableClosure L) :
        x ∈ E.separableClosureCongr e ↔ e.separableClosureCongr x ∈ E

        Membership in a transported subextension is tested in the original separable closure.

        source
        noncomputable def IntermediateField.separableClosureCongrEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) :
        ↥E ≃+* ↥(E.separableClosureCongr e)

        The chosen identification restricts to an isomorphism of the underlying fields.

        Instances For
          source
          @[simp]
          theorem IntermediateField.coe_separableClosureCongrEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) (x : ↥E) :
          ↑((E.separableClosureCongrEquiv e) x) = e.separableClosureCongr.symm ↑x

          The restricted field identification acts by the inverse separable-closure map.

          source
          @[simp]
          theorem IntermediateField.coe_separableClosureCongrEquiv_symm {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) (x : ↥(E.separableClosureCongr e)) :
          ↑((E.separableClosureCongrEquiv e).symm x) = e.separableClosureCongr ↑x

          The inverse restricted identification acts by the separable-closure map.

          source
          @[simp]
          theorem IntermediateField.separableClosureCongrEquiv_algebraMap {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) (r : K) :
          (E.separableClosureCongrEquiv e) ((algebraMap K ↥E) r) = (algebraMap L ↥(E.separableClosureCongr e)) (e r)

          The restricted identification extends the base-field isomorphism.

          source
          @[simp]
          theorem IntermediateField.separableClosureCongr_le_iff {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) {E F : IntermediateField K (SeparableClosure K)} :
          E.separableClosureCongr e ≤ F.separableClosureCongr e ↔ E ≤ F

          Transport preserves and reflects inclusion of subextensions.

          source
          theorem IntermediateField.separableClosureCongr_mono {K : Type u_1} {L : Type u_2} [Field K] [Field L] (e : K ≃+* L) {E F : IntermediateField K (SeparableClosure K)} (h : E ≤ F) :
          E.separableClosureCongr e ≤ F.separableClosureCongr e

          Refining a subextension refines its transported image.

          source
          @[simp]
          theorem IntermediateField.finrank_separableClosureCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) :
          Module.finrank L ↥(E.separableClosureCongr e) = Module.finrank K ↥E

          Transport along a field isomorphism preserves the degree.

          source
          instance IntermediateField.instFiniteDimensionalSeparableClosureCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) [FiniteDimensional K ↥E] :
          FiniteDimensional L ↥(E.separableClosureCongr e)

          A finite subextension remains finite after transport.

          source
          instance IntermediateField.instNormalSubtypeSeparableClosureMemSeparableClosureCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) [Normal K ↥E] :
          Normal L ↥(E.separableClosureCongr e)

          Normality is preserved by transport along a field isomorphism.

          source
          instance IntermediateField.instIsGaloisSubtypeSeparableClosureMemSeparableClosureCongrOfNormal {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) [Normal K ↥E] :
          IsGalois L ↥(E.separableClosureCongr e)

          A transported normal subextension is Galois, with separability inherited from the closure.

          source
          noncomputable def IntermediateField.separableClosureCongrAutEquiv {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) :
          Gal(↥E/K) ≃* Gal(↥(E.separableClosureCongr e)/L)

          Identify automorphisms by conjugating through the restricted field identification.

          Instances For
            source
            @[simp]
            theorem IntermediateField.separableClosureCongrAutEquiv_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) (g : Gal(↥E/K)) (x : ↥(E.separableClosureCongr e)) :
            ((E.separableClosureCongrAutEquiv e) g) x = (E.separableClosureCongrEquiv e) (g ((E.separableClosureCongrEquiv e).symm x))

            The transported automorphism acts by conjugation through the field identification.

            source
            @[simp]
            theorem IntermediateField.separableClosureCongrAutEquiv_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) (g : Gal(↥(E.separableClosureCongr e)/L)) (x : ↥E) :
            ((E.separableClosureCongrAutEquiv e).symm g) x = (E.separableClosureCongrEquiv e).symm (g ((E.separableClosureCongrEquiv e) x))

            The inverse automorphism transport acts by the reverse conjugation.

            source
            theorem IntermediateField.separableClosureCongrAutEquiv_restrictNormalHom {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) [Normal K ↥E] (g : TauCeti.AbsoluteGaloisGroup L) :
            (E.separableClosureCongrAutEquiv e) ((AlgEquiv.restrictNormalHom ↥E) (e.absoluteGaloisGroupCongr g)) = (AlgEquiv.restrictNormalHom ↥(E.separableClosureCongr e)) g

            Restriction to a normal subextension commutes with transport of the absolute Galois group.

            source
            theorem IntermediateField.fixingSubgroup_separableClosureCongr {K : Type u_1} {L : Type u_2} [Field K] [Field L] (E : IntermediateField K (SeparableClosure K)) (e : K ≃+* L) :
            (E.separableClosureCongr e).fixingSubgroup = Subgroup.comap e.absoluteGaloisGroupCongr.toMonoidHom E.fixingSubgroup

            Fixing subgroups are transported by the same absolute-Galois-group equivalence.