Module

OriginalFractionFieldGaloisTopology.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.OriginalFractionFieldGaloisTopology

3 declarations indexed from sourceView source ↗

Module documentation

The original fraction-field Galois comparison preserves the Krull topology

A finite intermediate field over the displayed fraction field is finite over the canonical fraction field because their coefficient map is surjective. The original scalar comparison therefore carries every basic Krull neighborhood continuously. Compactness gives continuity of its inverse.

The finite-basis argument adapts InfiniteGalois.restrictNormalHom_continuous from Mathlib/FieldTheory/Galois/Profinite.lean at revision 065356127b1dc0016f66b7283ce0ce2c4055aa55.

Imports4

Nyll.EtaleFundamentalGroups.StrictHenselian.OriginalFractionFieldGalois
Mathlib.FieldTheory.Galois.Profinite
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.Topology.Algebra.ContinuousMonoidHom

Imported by3

theorem

extendScalarsHomOfSurjective_continuous

L34 ↗

EtaleFundamentalGroups.StrictHenselian.extendScalarsHomOfSurjective_continuous

Source context 4 commands

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

noncomputable section
open scoped Topology
namespace EtaleFundamentalGroups.StrictHenselian
universe u v w

Lean source · statement

theorem extendScalarsHomOfSurjective_continuous
    (F : Type u) (K : Type v) (L : Type w) [Field F] [Field K] [Field L]
    [Algebra F K] [Algebra K L] [Algebra F L] [IsScalarTower F K L]
    (h : Function.Surjective (algebraMap F K)) :
    Continuous (AlgEquiv.extendScalarsHomOfSurjective (A := L) h :
      Gal(L/F) ≃* Gal(L/K))

theorem

originalFractionFieldGaloisEquiv_continuous

L59 ↗

EtaleFundamentalGroups.StrictHenselian.originalFractionFieldGaloisEquiv_continuous

Documentation

The canonical-to-original fraction-field Galois comparison is continuous for the original Krull topologies.

Source context 4 commands

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

noncomputable section
open scoped Topology
namespace EtaleFundamentalGroups.StrictHenselian
universe u v w

Lean source · full declaration

theorem originalFractionFieldGaloisEquiv_continuous
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra A L] [FaithfulSMul A L]
    [Algebra K L] [IsScalarTower A K L] :
    let : Algebra (FractionRing A) K := FractionRing.liftAlgebra A K
    let : Algebra (FractionRing A) L := FractionRing.liftAlgebra A L
    Continuous (originalFractionFieldGaloisEquiv A K L) := by
  intro actualFractionAlgebra actualAmbientAlgebra
  have : IsScalarTower (FractionRing A) K L := inferInstance
  exact extendScalarsHomOfSurjective_continuous (FractionRing A) K L
    (fractionFieldBaseMap_surjective A K)

theorem

originalFractionFieldGaloisEquiv_isHomeomorph

L74 ↗

EtaleFundamentalGroups.StrictHenselian.originalFractionFieldGaloisEquiv_isHomeomorph

Documentation

The same literal original automorphism comparison is a homeomorphism when the ambient field is the original separable closure.

Source context 4 commands

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

noncomputable section
open scoped Topology
namespace EtaleFundamentalGroups.StrictHenselian
universe u v w

Lean source · full declaration

theorem originalFractionFieldGaloisEquiv_isHomeomorph
    (A : Type u) (K : Type v) (L : Type w)
    [CommRing A] [IsDomain A] [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K] [Algebra A L] [FaithfulSMul A L]
    [Algebra K L] [IsScalarTower A K L] [IsGalois K L] [IsSepClosed L] :
    let : Algebra (FractionRing A) K := FractionRing.liftAlgebra A K
    let : Algebra (FractionRing A) L := FractionRing.liftAlgebra A L
    IsHomeomorph (originalFractionFieldGaloisEquiv A K L) := by
  intro actualFractionAlgebra actualAmbientAlgebra
  have : IsSepClosure (FractionRing A) L := originalFractionField_isSepClosure A K L
  rw [isHomeomorph_iff_continuous_bijective]
  exact ⟨originalFractionFieldGaloisEquiv_continuous A K L,
    (originalFractionFieldGaloisEquiv A K L).bijective⟩

Module documentation

The original fraction-field Galois comparison preserves the Krull topology

Declarations

extendScalarsHomOfSurjective_continuous

originalFractionFieldGaloisEquiv_continuous

originalFractionFieldGaloisEquiv_isHomeomorph