NYLL
Module

NativeFiniteNormalizationTameProperties.lean

Nyll.EtaleFundamentalGroups.Inertia.NativeFiniteNormalizationTameProperties
7 declarations indexed from sourceView source ↗

Module documentation

Finite normalization and intrinsic tame orders

Establishes module and automorphism finiteness for native finite normalizations, then proves positivity and base-ring invertibility of their intrinsic tame orders.

Imports6
Imported by12

Declarations

theorem

nativeFieldNormalization_isDedekindDomain

L28 ↗
EtaleFundamentalGroups.Inertia.nativeFieldNormalization_isDedekindDomain
Documentation

A finite field extension supplies the Dedekind structure on its actual normalization.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem nativeFieldNormalization_isDedekindDomain
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDedekindDomain A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [FiniteDimensional K F] [Algebra.IsSeparable K F] :
    IsDedekindDomain (normalizationCommAlgCat A F).carrier
theorem

nativeFieldNormalization_isTorsionFree

L37 ↗
EtaleFundamentalGroups.Inertia.nativeFieldNormalization_isTorsionFree
Documentation

The actual fraction-field tower supplies torsion freeness of its normalization.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem nativeFieldNormalization_isTorsionFree
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] :
    Module.IsTorsionFree A (normalizationCommAlgCat A F).carrier
theorem

nativeFieldNormalization_isGaloisGroup

L47 ↗
EtaleFundamentalGroups.Inertia.nativeFieldNormalization_isGaloisGroup
Documentation

The actual finite Galois field extension supplies the intrinsic normalization Galois action.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
Lean source · statement
theorem nativeFieldNormalization_isGaloisGroup
    (A : Type u) (K : Type v) (F : Type w)
    [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [Field K] [Field F]
    [Algebra A K] [IsFractionRing A K] [Algebra K F] [Algebra A F]
    [IsScalarTower A K F] [FiniteDimensional K F] [IsGalois K F] :
    IsGaloisGroup ((normalizationCommAlgCat A F).carrier ≃ₐ[A]
      (normalizationCommAlgCat A F).carrier) A (normalizationCommAlgCat A F).carrier
theorem

nativeNormalization_finite

L65 ↗
EtaleFundamentalGroups.Inertia.nativeNormalization_finite
Documentation

Native integral-closure finiteness before any inertia or prime is opened.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) [CommRing A] [IsDedekindDomain A]
  (K : Type v) [Field K] [Algebra A K] [IsFractionRing A K]
  (C : CommAlgCat.{w} A) (hC : IsField C.carrier) [Algebra K C.carrier]
  [IsScalarTower A K C.carrier]
  [FiniteDimensional K C.carrier] [Algebra.IsSeparable K C.carrier]
include K hC
Lean source · statement
theorem nativeNormalization_finite :
    Module.Finite A (normalizationCommAlgCat A C.carrier).carrier
theorem

nativeNormalization_aut_finite

L72 ↗
EtaleFundamentalGroups.Inertia.nativeNormalization_aut_finite
Documentation

The intrinsic automorphism group of the actual finite normalization is finite by the native finite-integral-domain automorphism theorem.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) [CommRing A] [IsDedekindDomain A]
  (K : Type v) [Field K] [Algebra A K] [IsFractionRing A K]
  (C : CommAlgCat.{w} A) (hC : IsField C.carrier) [Algebra K C.carrier]
  [IsScalarTower A K C.carrier]
  [FiniteDimensional K C.carrier] [Algebra.IsSeparable K C.carrier]
include K hC
Lean source · statement
theorem nativeNormalization_aut_finite :
    Finite ((normalizationCommAlgCat A C.carrier).carrier ≃ₐ[A]
      (normalizationCommAlgCat A C.carrier).carrier)
theorem

nativeFiniteNormalizationTameOrder_pos

L86 ↗
EtaleFundamentalGroups.Inertia.nativeFiniteNormalizationTameOrder_pos
Documentation

Every nonzero prime of this actual finite normalization has positive intrinsic tame order. The original upper prime has not been introduced.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) [CommRing A] [IsDedekindDomain A]
  (K : Type v) [Field K] [Algebra A K] [IsFractionRing A K]
  (C : CommAlgCat.{w} A) (hC : IsField C.carrier) [Algebra K C.carrier]
  [IsScalarTower A K C.carrier]
  [FiniteDimensional K C.carrier] [Algebra.IsSeparable K C.carrier]
include K hC
Lean source · full declaration
theorem nativeFiniteNormalizationTameOrder_pos
    (Q : Ideal (normalizationCommAlgCat A C)) [Q.IsPrime] (hQ : Q ≠ ⊥) :
    letI : Field C := hC.toField
    let : IsDedekindDomain (normalizationCommAlgCat A C) :=
      integralClosure.isDedekindDomain A K C
    0 < commAlgIdealTameOrder A (normalizationCommAlgCat A C) Q hQ := by
  let : Field C := hC.toField
  let : IsDedekindDomain (normalizationCommAlgCat A C) :=
    integralClosure.isDedekindDomain A K C
  have := nativeNormalization_aut_finite A K C hC
  exact commAlgIdealTameOrder_pos A (normalizationCommAlgCat A C) Q hQ
theorem

nativeFiniteNormalizationTameOrder_isUnit

L99 ↗
EtaleFundamentalGroups.Inertia.nativeFiniteNormalizationTameOrder_isUnit
Documentation

Its actual tame order is invertible in the original local base ring.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
variable (A : Type u) [CommRing A] [IsDedekindDomain A]
  (K : Type v) [Field K] [Algebra A K] [IsFractionRing A K]
  (C : CommAlgCat.{w} A) (hC : IsField C.carrier) [Algebra K C.carrier]
  [IsScalarTower A K C.carrier]
  [FiniteDimensional K C.carrier] [Algebra.IsSeparable K C.carrier]
include K hC
Lean source · full declaration
theorem nativeFiniteNormalizationTameOrder_isUnit [IsLocalRing A]
    (Q : Ideal (normalizationCommAlgCat A C)) [Q.IsPrime]
    (hQ : Q ≠ ⊥) :
    letI : Field C := hC.toField
    let : IsDedekindDomain (normalizationCommAlgCat A C) :=
      integralClosure.isDedekindDomain A K C
    IsUnit (commAlgIdealTameOrder A (normalizationCommAlgCat A C) Q hQ : A) := by
  let : Field C := hC.toField
  let : IsDedekindDomain (normalizationCommAlgCat A C) :=
    integralClosure.isDedekindDomain A K C
  have := nativeNormalization_aut_finite A K C hC
  have : Q.IsMaximal := Ideal.IsPrime.isMaximal inferInstance hQ
  have := normalizationCommAlgCat_liesOver_maximalIdeal Q
  exact commAlgIdealTameOrder_isUnit A (normalizationCommAlgCat A C) Q hQ

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