NYLL
Module

Component.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.Component
11 declarations indexed from sourceView source ↗

Module documentation

A specified generic component of a finite etale algebra

For a finite etale algebra over a normal domain, a maximal ideal of the generic fibre selects one field component. This file descends the primitive idempotent of that specified component through smooth integral-closure base change. The selected component normalization is thereby an actual idempotent factor of the original finite etale algebra.

Imports3
Imported by9

Declarations

def

artinianSelectedComponentIdempotent

L36 ↗
EtaleFundamentalGroups.artinianSelectedComponentIdempotent
Documentation

The primitive idempotent supported at a specified maximal ideal of a reduced Artinian ring.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section ArtinianComponent
variable {G : Type*} [CommRing G] [IsArtinianRing G] [IsReduced G]
Lean source · statement
def artinianSelectedComponentIdempotent
    (m : Ideal G) [m.IsMaximal] : G
theorem

quotient_artinianSelectedComponentIdempotent_eq_zero

L42 ↗
EtaleFundamentalGroups.quotient_artinianSelectedComponentIdempotent_eq_zero
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section ArtinianComponent
variable {G : Type*} [CommRing G] [IsArtinianRing G] [IsReduced G]
Lean source · statement
theorem quotient_artinianSelectedComponentIdempotent_eq_zero
    (m : Ideal G) [m.IsMaximal] (M : MaximalSpectrum G)
    (hM : M ≠ (⟨m, inferInstance⟩ : MaximalSpectrum G)) :
    Ideal.Quotient.mk M.asIdeal
        (artinianSelectedComponentIdempotent m) = 0
theorem

quotient_artinianSelectedComponentIdempotent

L63 ↗
EtaleFundamentalGroups.quotient_artinianSelectedComponentIdempotent
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section ArtinianComponent
variable {G : Type*} [CommRing G] [IsArtinianRing G] [IsReduced G]
Lean source · statement
theorem quotient_artinianSelectedComponentIdempotent
    (m : Ideal G) [m.IsMaximal] :
    Ideal.Quotient.mk m (artinianSelectedComponentIdempotent m) = 1
theorem

artinianSelectedComponentIdempotent_isIdempotentElem

L82 ↗
EtaleFundamentalGroups.artinianSelectedComponentIdempotent_isIdempotentElem
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section ArtinianComponent
variable {G : Type*} [CommRing G] [IsArtinianRing G] [IsReduced G]
Lean source · statement
theorem artinianSelectedComponentIdempotent_isIdempotentElem
    (m : Ideal G) [m.IsMaximal] :
    IsIdempotentElem (artinianSelectedComponentIdempotent m)
theorem

artinianSelectedComponentIdempotent_mul_eq_zero_iff

L98 ↗
EtaleFundamentalGroups.artinianSelectedComponentIdempotent_mul_eq_zero_iff
Documentation

Multiplication by the selected primitive idempotent kills exactly the elements vanishing in the specified field component.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section ArtinianComponent
variable {G : Type*} [CommRing G] [IsArtinianRing G] [IsReduced G]
Lean source · statement
theorem artinianSelectedComponentIdempotent_mul_eq_zero_iff
    (m : Ideal G) [m.IsMaximal] (x : G) :
    artinianSelectedComponentIdempotent m * x = 0 ↔
      Ideal.Quotient.mk m x = 0
theorem

exists_integral_artinianElement_supported_at_component

L120 ↗
EtaleFundamentalGroups.exists_integral_artinianElement_supported_at_component
Documentation

An integral element of a specified residue-field component, extended by zero on every other Artinian component, is represented by an integral element of the whole Artinian ring.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section ArtinianComponent
variable {G : Type*} [CommRing G] [IsArtinianRing G] [IsReduced G]
Lean source · statement
theorem exists_integral_artinianElement_supported_at_component
    {R : Type uR} [CommRing R] [Algebra R G]
    (m : Ideal G) [m.IsMaximal]
    (x : G ⧸ m) (hx : IsIntegral R x) :
    ∃ y : G, IsIntegral R y ∧ Ideal.Quotient.mk m y = x
abbrev

FiniteEtaleGenericFiberComponent

L170 ↗
EtaleFundamentalGroups.FiniteEtaleGenericFiberComponent
Documentation

The field component of the generic fibre selected by a maximal ideal.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section FiniteEtaleComponent
variable {R : Type uR} {T : Type uT} {K : Type uK}
Lean source · statement
abbrev FiniteEtaleGenericFiberComponent
    [CommRing R] [CommRing T] [Algebra R T]
    [Field K] [Algebra R K]
    (m : Ideal (T ⊗[R] K))
def

genericFiberComponentToIntegralClosure

L177 ↗
EtaleFundamentalGroups.genericFiberComponentToIntegralClosure
Documentation

The finite-etale algebra maps canonically to the integral closure of the base in a selected generic-fibre component.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section FiniteEtaleComponent
variable {R : Type uR} {T : Type uT} {K : Type uK}
Lean source · statement
def genericFiberComponentToIntegralClosure
    [CommRing R] [CommRing T] [Algebra R T] [Module.Finite R T]
    [Field K] [Algebra R K]
    (m : Ideal (T ⊗[R] K)) :
    T →ₐ[R] integralClosure R (FiniteEtaleGenericFiberComponent m)
theorem

genericFiberComponentToIntegralClosure_core

L188 ↗
EtaleFundamentalGroups.genericFiberComponentToIntegralClosure_core
Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section FiniteEtaleComponent
variable {R : Type uR} {T : Type uT} {K : Type uK}
Lean source · statement
theorem genericFiberComponentToIntegralClosure_core
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing T] [Algebra R T] [Module.Finite R T] [Algebra.Etale R T]
    [Field K] [Algebra R K] [IsFractionRing R K]
    (m : Ideal (T ⊗[R] K)) [m.IsMaximal] :
    Function.Surjective (genericFiberComponentToIntegralClosure m) ∧
      Algebra.Etale R
        (integralClosure R (FiniteEtaleGenericFiberComponent m))
theorem

genericFiberComponentToIntegralClosure_surjective

L275 ↗
EtaleFundamentalGroups.genericFiberComponentToIntegralClosure_surjective
Documentation

The canonical map to the normalization of a selected generic-fibre component is surjective; equivalently, that normalization is an idempotent factor of the original finite-etale algebra.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section FiniteEtaleComponent
variable {R : Type uR} {T : Type uT} {K : Type uK}
Lean source · statement
theorem genericFiberComponentToIntegralClosure_surjective
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing T] [Algebra R T] [Module.Finite R T] [Algebra.Etale R T]
    [Field K] [Algebra R K] [IsFractionRing R K]
    (m : Ideal (T ⊗[R] K)) [m.IsMaximal] :
    Function.Surjective (genericFiberComponentToIntegralClosure m)
theorem

integralClosure_etale_genericFiberComponent

L289 ↗
EtaleFundamentalGroups.integralClosure_etale_genericFiberComponent
Documentation

The normalization of a specified field component of the generic fibre of a finite etale algebra is itself finite etale over the base.

More precisely, the proof descends the primitive idempotent of the specified generic component to T, and realizes the integral closure as the associated idempotent localization of T.

Source context 7 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uT uK
section FiniteEtaleComponent
variable {R : Type uR} {T : Type uT} {K : Type uK}
Lean source · statement
theorem integralClosure_etale_genericFiberComponent
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing T] [Algebra R T] [Module.Finite R T] [Algebra.Etale R T]
    [Field K] [Algebra R K] [IsFractionRing R K]
    (m : Ideal (T ⊗[R] K)) [m.IsMaximal] :
    Algebra.Etale R
      (integralClosure R (FiniteEtaleGenericFiberComponent m))

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