NYLL
Module

SemilinearConjugationTopology.lean

Nyll.GaloisCohomology.Kummer.Concrete.SemilinearConjugationTopology
3 declarations indexed from sourceView source ↗

Module documentation

Continuity of semilinear Galois conjugation

The inverse images of a basis of a finite intermediate field generate a finite intermediate field. Its fixing subgroup maps into the original fixing subgroup under semilinear conjugation. This proves continuity for the Krull topology without putting a topology on the extension field.

Imports5
Imported by6

Declarations

theorem

semilinearGaloisConjugateEquiv_continuous

L30 ↗
KummerTheory.semilinearGaloisConjugateEquiv_continuous
Documentation

Semilinear conjugation is continuous for the Krull topology.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
  [Algebra.IsAlgebraic K Ω]
Lean source · statement
theorem semilinearGaloisConjugateEquiv_continuous (τ : K ≃+* K) (e : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k)) :
    Continuous (semilinearGaloisConjugateEquiv τ e he)
def

semilinearGaloisConjugateContinuousEquiv

L65 ↗
KummerTheory.semilinearGaloisConjugateContinuousEquiv
Documentation

Semilinear conjugation is a continuous automorphism of the relative Galois group, including continuity of its inverse.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
  [Algebra.IsAlgebraic K Ω]
Lean source · full declaration
def semilinearGaloisConjugateContinuousEquiv (τ : K ≃+* K) (e : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k)) :
    Gal(Ω/K) ≃ₜ* Gal(Ω/K) where
  toMulEquiv := semilinearGaloisConjugateEquiv τ e he
  continuous_toFun := semilinearGaloisConjugateEquiv_continuous τ e he
  continuous_invFun := semilinearGaloisConjugateEquiv_continuous τ.symm e.symm
    (semilinear_symm_algebraMap τ e he)
theorem

semilinearGaloisConjugateContinuousEquiv_apply

L75 ↗
KummerTheory.semilinearGaloisConjugateContinuousEquiv_apply
Documentation

The continuous conjugation evaluates by the constructed algebraic conjugation.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace KummerTheory
open scoped Topology
variable {K Ω : Type*} [Field K] [Field Ω] [Algebra K Ω]
  [Algebra.IsAlgebraic K Ω]
Lean source · statement
theorem semilinearGaloisConjugateContinuousEquiv_apply (τ : K ≃+* K) (e : Ω ≃+* Ω)
    (he : ∀ k : K, e (algebraMap K Ω k) = algebraMap K Ω (τ k))
    (σ : Gal(Ω/K)) :
    semilinearGaloisConjugateContinuousEquiv τ e he σ =
      semilinearGaloisConjugate τ e he σ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.