Maximal unramified subextension

DefinitionFinite unramified intermediate fields#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a field extension such that the map \(A \to L\) factors as \(A \to K \to L\). An intermediate field \(E\) of \(L/K\) is finite unramified relative to \(A\) if \(E\) is finite-dimensional over \(K\) and the integral closure of \(A\) in \(E\) is formally unramified over \(A\).

def IsFiniteUnramified (A : Type*) {K L : Type*} [CommRing A] [Field K] [Field L]
    [Algebra A K] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    (E : IntermediateField K L) : Prop :=
  FiniteDimensional K E ∧ Algebra.FormallyUnramified A (integralClosure A E)

Used by 5

Used byFinite unramified subfields lie in the maximal unramified subextension · Automorphisms preserve finite unramified subfields · The maximal unramified subextension is stable under automorphisms · Maximal unramified subextension · Universal property of the maximal unramified subextension

DefinitionMaximal unramified subextension#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a field extension such that the map \(A \to L\) factors as \(A \to K \to L\). The maximal unramified subextension of \(L/K\) relative to \(A\) is the supremum, in the lattice of intermediate fields of \(L/K\), of all intermediate fields of \(L/K\) that are finite unramified relative to \(A\).

The supremum need not itself be finite or formally unramified.

noncomputable def maximalUnramifiedSubextension (A K L : Type*) [CommRing A]
    [Field K] [Field L] [Algebra A K] [Algebra A L] [Algebra K L]
    [IsScalarTower A K L] : IntermediateField K L :=
  ⨆ (E : IntermediateField K L) (_ : IsFiniteUnramified A E), E

Uses 1 · Used by 3

Statement usesFinite unramified intermediate fields

Used byFinite unramified subfields lie in the maximal unramified subextension · The maximal unramified subextension is stable under automorphisms · Universal property of the maximal unramified subextension

TheoremFinite unramified subfields lie in the maximal unramified subextension#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a field extension such that the map \(A \to L\) factors as \(A \to K \to L\). Every intermediate field \(E\) of \(L/K\) that is finite unramified relative to \(A\) is contained in the maximal unramified subextension of \(L/K\) relative to \(A\).

theorem le_maximalUnramifiedSubextension {E : IntermediateField K L}
    (hE : IsFiniteUnramified A E) :
    E ≤ maximalUnramifiedSubextension A K L

Uses 2 · Used by 2

Statement usesFinite unramified intermediate fields · Maximal unramified subextension

Used byThe maximal unramified subextension is stable under automorphisms · Universal property of the maximal unramified subextension

TheoremUniversal property of the maximal unramified subextension#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a field extension such that the map \(A \to L\) factors as \(A \to K \to L\). An intermediate field \(F\) of \(L/K\) contains the maximal unramified subextension of \(L/K\) relative to \(A\) if and only if \(F\) contains every intermediate field of \(L/K\) that is finite unramified relative to \(A\).

@[simp]
theorem maximalUnramifiedSubextension_le_iff {F : IntermediateField K L} :
    maximalUnramifiedSubextension A K L ≤ F ↔
      ∀ E : IntermediateField K L, IsFiniteUnramified A E → E ≤ F

Uses 3

Statement usesFinite unramified intermediate fields · Maximal unramified subextension

Proof usesFinite unramified subfields lie in the maximal unramified subextension

TheoremAutomorphisms preserve finite unramified subfields#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a field extension such that the map \(A \to L\) factors as \(A \to K \to L\). If an intermediate field \(E\) of \(L/K\) is finite unramified relative to \(A\), then for every \(K\)-algebra automorphism \(\sigma\) of \(L\) the image \(\sigma(E)\) is finite unramified relative to \(A\).

theorem IsFiniteUnramified.map {E : IntermediateField K L}
    (hE : IsFiniteUnramified A E) (σ : L ≃ₐ[K] L) :
    IsFiniteUnramified A (E.map σ.toAlgHom)

Uses 1 · Used by 1

Statement usesFinite unramified intermediate fields

Used byThe maximal unramified subextension is stable under automorphisms

TheoremThe maximal unramified subextension is stable under automorphisms#✓fully proved

Let \(A\) be a commutative ring and \(L/K\) a field extension such that the map \(A \to L\) factors as \(A \to K \to L\), and let \(M\) be the maximal unramified subextension of \(L/K\) relative to \(A\). For every \(K\)-algebra automorphism \(\sigma\) of \(L\), \(\sigma(M) = M\).

theorem map_maximalUnramifiedSubextension (σ : L ≃ₐ[K] L) :
    (maximalUnramifiedSubextension A K L).map σ.toAlgHom =
      maximalUnramifiedSubextension A K L

Uses 4

Statement usesMaximal unramified subextension

Proof usesFinite unramified intermediate fields · Automorphisms preserve finite unramified subfields · Finite unramified subfields lie in the maximal unramified subextension

6 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.