NYLL
Module

FiniteNormalizationActionDiagram.lean

Nyll.EtaleFundamentalGroups.Inertia.FiniteNormalizationActionDiagram
19 declarations indexed from sourceView source ↗

Module documentation

Actual finite-normalization ring-action diagrams

The field constructors are finished before the ordinary ring/group image argument. All groups, rings, actions, maps, and primes are the existing literal objects. Every non-data input to the ordinary image theorem is proved below; no inertia-image theorem is used as a supplier.

Imports14
Imported by5

Declarations

theorem

finiteGaloisIntermediateField_isField

L47 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisIntermediateField_isField
Documentation

The actual finite level is a field, proved before coefficient algebras and normalization rings enter the scope.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section FieldOnly
variable (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteGaloisIntermediateField_isField (E : FiniteGaloisIntermediateField K L) :
    IsField E
def

finiteGaloisFixingTopology

L52 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisFixingTopology
Documentation

The prescribed Krull subspace topology on the actual fixing subgroup.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section FieldOnly
variable (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
Lean source · statement
def finiteGaloisFixingTopology (E : FiniteGaloisIntermediateField K L) :
    TopologicalSpace E.toIntermediateField.fixingSubgroup
theorem

finiteGaloisRestrictionGroupMap_surjective

L56 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisRestrictionGroupMap_surjective
Documentation

Original field restriction is surjective, in a scope without normalization data.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section FieldOnly
variable (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteGaloisRestrictionGroupMap_surjective [IsGalois K L]
    (E : FiniteGaloisIntermediateField K L) :
    Function.Surjective (finiteGaloisRestrictionGroupMap K L E).hom'.toFun
theorem

finiteGaloisRestrictionGroupMap_fixes_kernel

L62 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisRestrictionGroupMap_fixes_kernel
Documentation

The actual fixing subgroup is killed by the actual field restriction.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section FieldOnly
variable (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteGaloisRestrictionGroupMap_fixes_kernel
    (E : FiniteGaloisIntermediateField K L) :
    ∀ g : (galoisGroupObject K L).carrier,
      E.toIntermediateField.fixingSubgroup.carrier g →
      (finiteGaloisRestrictionGroupMap K L E).hom'.toFun g = 1
theorem

finiteGaloisFixingTopology_compact

L71 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisFixingTopology_compact
Documentation

Compactness of the actual kernel, proved before ring actions occur.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section FieldOnly
variable (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
Lean source · full declaration
theorem finiteGaloisFixingTopology_compact [IsGalois K L]
    (E : FiniteGaloisIntermediateField K L) :
    let : TopologicalSpace E.toIntermediateField.fixingSubgroup := finiteGaloisFixingTopology K L E
    CompactSpace E.toIntermediateField.fixingSubgroup := by
  intro kernelTopology
  exact isCompact_iff_compactSpace.mp
    (IntermediateField.fixingSubgroup_isClosed E.toIntermediateField).isCompact
theorem

finiteGaloisFixingTopology_totallyDisconnected

L80 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisFixingTopology_totallyDisconnected
Documentation

The actual kernel inherits total disconnectedness from the Krull topology.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section FieldOnly
variable (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
Lean source · full declaration
theorem finiteGaloisFixingTopology_totallyDisconnected [IsGalois K L]
    (E : FiniteGaloisIntermediateField K L) :
    let : TopologicalSpace E.toIntermediateField.fixingSubgroup := finiteGaloisFixingTopology K L E
    TotallyDisconnectedSpace E.toIntermediateField.fixingSubgroup := by
  intro kernelTopology
  infer_instance
theorem

finiteGaloisFixingTopology_isTopologicalGroup

L88 ↗
EtaleFundamentalGroups.Inertia.finiteGaloisFixingTopology_isTopologicalGroup
Documentation

The actual kernel inherits its topological group structure.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section FieldOnly
variable (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
Lean source · full declaration
theorem finiteGaloisFixingTopology_isTopologicalGroup
    (E : FiniteGaloisIntermediateField K L) :
    let : TopologicalSpace E.toIntermediateField.fixingSubgroup := finiteGaloisFixingTopology K L E
    IsTopologicalGroup E.toIntermediateField.fixingSubgroup := by
  intro kernelTopology
  infer_instance
theorem

finiteField_mem_of_fixed

L97 ↗
EtaleFundamentalGroups.Inertia.finiteField_mem_of_fixed
Documentation

The infinite Galois correspondence detects membership in the literal intermediate field, before any integral closure is introduced.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section FieldOnly
variable (K : Type v) (L : Type w) [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem finiteField_mem_of_fixed [IsGalois K L]
    (E : FiniteGaloisIntermediateField K L) (x : L)
    (h : ∀ g : Gal(L/K), E.toIntermediateField.fixingSubgroup.carrier g →
      g.toRingHom.toFun x = x) : x ∈ E.toIntermediateField
theorem

subalgebraNormalization_preimage_of_mem

L112 ↗
EtaleFundamentalGroups.Inertia.subalgebraNormalization_preimage_of_mem
Documentation

A coefficient already in the literal subalgebra has an integral preimage in its literal normalization. No fraction field is involved.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section RingOnly
variable {A : Type u} {L : Type w} [CommRing A] [CommRing L] [Algebra A L]
Lean source · statement
theorem subalgebraNormalization_preimage_of_mem
    (S : Subalgebra A L) (b : integralClosure A L) (hb : S.carrier b.val) :
    ∃ c : (subalgebraNormalizationCommAlgCat S).carrier,
      (subalgebraNormalizationRingMap S).toFun c = b
def

finiteNormalizationOriginalAction

L135 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationOriginalAction
Documentation

The original finite normalization action, retained on the already constructed native finite group and normalization carriers.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
def finiteNormalizationOriginalAction (E : FiniteGaloisIntermediateField K L) :
    MulSemiringAction (finiteGaloisGroupObject K L E).carrier
      (finiteAbsoluteNormalizationAlgebra A K L E).carrier
def

finiteNormalizationActionDiagram

L142 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationActionDiagram
Documentation

The original ordinary ring-action data, with no theorem or comparison fields.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · full declaration
def finiteNormalizationActionDiagram (E : FiniteGaloisIntermediateField K L) :
    RingActionRestriction.{w, w, w, w} where
  lowerRing := CommRingCat.of (finiteAbsoluteNormalizationAlgebra A K L E).carrier
  upperRing := CommRingCat.of (normalizationCommAlgCat A L).carrier
  upperGroup := galoisGroupObject K L
  lowerGroup := finiteGaloisGroupObject K L E
  upperAction := normalizationInertiaImageAction A K L
  lowerAction := finiteNormalizationOriginalAction A K L E
  ringMap := finiteAbsoluteNormalizationRingMap A K L E
  groupMap := (finiteGaloisRestrictionGroupMap K L E).hom'
  kernelGroup := E.toIntermediateField.fixingSubgroup
  kernelTopology := finiteGaloisFixingTopology K L E
theorem

originalNormalization_fixed_coefficient

L157 ↗
EtaleFundamentalGroups.Inertia.originalNormalization_fixed_coefficient
Documentation

Fixedness for the original action is detected on the literal coefficient. The action square is the already proved actual normalization square.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
theorem originalNormalization_fixed_coefficient
    (g : Gal(L/K)) (b : integralClosure A L) (hb : g • b = b) :
    g.toRingHom.toFun b.val = b.val
theorem

finiteNormalizationOriginalAction_ringHom

L168 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationOriginalAction_ringHom
Documentation

The original finite-action ring map agrees with the existing finite normalization automorphism map, in a scope without the upper normalization.

Source context 8 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
omit [IsGalois K L] in
Lean source · full declaration
theorem finiteNormalizationOriginalAction_ringHom
    (E : FiniteGaloisIntermediateField K L)
    (g : (finiteGaloisGroupObject K L E).carrier) :
    let : MulSemiringAction (finiteGaloisGroupObject K L E).carrier
        (finiteAbsoluteNormalizationAlgebra A K L E).carrier :=
      finiteNormalizationOriginalAction A K L E
    MulSemiringAction.toRingHom (finiteGaloisGroupObject K L E).carrier
        (finiteAbsoluteNormalizationAlgebra A K L E).carrier g =
      commAlgAutomorphismRingHom A (finiteAbsoluteNormalizationAlgebra A K L E)
        ((finiteNormalizationGaloisGroupMap A K L E).hom'.toFun g) := by
  intro finiteAction
  exact nativeNormalizationOriginalAction_ringHom A K (finiteLevelFieldAlgebra A K L E)
    (tAKC := finiteLevelFieldAlgebra_tower A K L E)
    (finiteGaloisIntermediateField_isField K L E) g
theorem

finiteNormalizationActionDiagram_contraction

L184 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationActionDiagram_contraction
Documentation

The literal prime contraction supplies the ordinary contraction premise.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
theorem finiteNormalizationActionDiagram_contraction
    (E : FiniteGaloisIntermediateField K L) (Q : Ideal (integralClosure A L)) :
    ∀ a : (finiteNormalizationActionDiagram A K L E).lowerRing.carrier,
      (finiteAbsoluteNormalizationPrime A K L Q E).carrier a ↔
        Q.carrier ((finiteNormalizationActionDiagram A K L E).ringMap.toFun a)
theorem

finiteNormalizationActionDiagram_fixedPreimages

L194 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationActionDiagram_fixedPreimages
Documentation

Actual fixed-element lifting is obtained from the infinite Galois correspondence followed by the ring-only integral preimage construction.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
theorem finiteNormalizationActionDiagram_fixedPreimages
    (E : FiniteGaloisIntermediateField K L) :
    (finiteNormalizationActionDiagram A K L E).HasFixedPreimages
theorem

finiteNormalizationActionDiagram_openFixedSets

L207 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationActionDiagram_openFixedSets
Documentation

The inherited kernel action has open fixed sets, by the already proved openness of the original normalization stabilizers and subtype continuity.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
theorem finiteNormalizationActionDiagram_openFixedSets
    (E : FiniteGaloisIntermediateField K L) :
    (finiteNormalizationActionDiagram A K L E).HasOpenFixedSets
theorem

finiteNormalizationActionDiagram_equivariant

L217 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationActionDiagram_equivariant
Documentation

The actual finite coefficient square proves diagram equivariance; no field-extension scalar structures are opened in this proof.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
theorem finiteNormalizationActionDiagram_equivariant
    (E : FiniteGaloisIntermediateField K L) :
    (finiteNormalizationActionDiagram A K L E).IsEquivariant
theorem

finiteNormalizationActionDiagram_images

L231 ↗
EtaleFundamentalGroups.Inertia.finiteNormalizationActionDiagram_images
Documentation

Both actual decomposition and inertia images are obtained by the ordinary ring/group theorem after all concrete suppliers are established.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · full declaration
theorem finiteNormalizationActionDiagram_images
    (Q : Ideal (normalizationCommAlgCat A L).carrier) [hQ : Q.IsPrime]
    (E : FiniteGaloisIntermediateField K L) :
    let D := finiteNormalizationActionDiagram A K L E
    (D.upperDecomposition Q).map D.groupMap =
        D.lowerDecomposition (finiteAbsoluteNormalizationPrime A K L Q E) ∧
      (D.upperInertia Q).map D.groupMap =
        D.lowerInertia (finiteAbsoluteNormalizationPrime A K L Q E) := by
  intro D
  exact RingActionRestriction.images_of_profinite D
    (finiteAbsoluteNormalizationPrime A K L Q E) Q (hq := hQ)
    (finiteGaloisFixingTopology_compact K L E)
    (finiteGaloisFixingTopology_totallyDisconnected K L E)
    (finiteGaloisFixingTopology_isTopologicalGroup K L E)
    (finiteNormalizationActionDiagram_contraction A K L E Q)
    (finiteNormalizationActionDiagram_fixedPreimages A K L E)
    (finiteNormalizationActionDiagram_openFixedSets A K L E)
    (finiteGaloisRestrictionGroupMap_surjective K L E)
    (finiteGaloisRestrictionGroupMap_fixes_kernel K L E)
    (finiteNormalizationActionDiagram_equivariant A K L E)
theorem

actualNormalizationInertia_exists_finiteNative_restriction

L255 ↗
EtaleFundamentalGroups.Inertia.actualNormalizationInertia_exists_finiteNative_restriction
Documentation

A finite native field-inertia element has an original inertia lift under the existing finite group restriction. The statement never opens the finite field's scalar or field dictionaries.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Inertia
open SchemeTheory
universe u v w
attribute [local instance] normalizationInertiaImageAction
section ActualData
variable (A : Type u) (K : Type v) (L : Type w)
  [CommRing A] [Field K] [Field L]
  [Algebra A K] [IsFractionRing A K]
  [Algebra K L] [Algebra A L] [IsScalarTower A K L] [IsGalois K L]
Lean source · statement
theorem actualNormalizationInertia_exists_finiteNative_restriction
    (Q : Ideal (integralClosure A L)) [hQ : Q.IsPrime]
    (E : FiniteGaloisIntermediateField K L)
    (τ : { g : (finiteGaloisGroupObject K L E).carrier //
      ((finiteNormalizationActionDiagram A K L E).lowerInertia
        (finiteAbsoluteNormalizationPrime A K L Q E)).carrier g }) :
    ∃ σ : (actualNormalizationInertiaGroup A K L Q).carrier,
      (finiteGaloisRestrictionGroupMap K L E).hom'.toFun
          (actualNormalizationInertiaElement A K L Q σ) = τ.val

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