NYLL
Module

TraceDual.lean

Nyll.SchemeTheory.Normalization.IntegralClosure.RegularPair.TraceDual
4 declarations indexed from sourceView source ↗

Module documentation

Regular pairs on a finite normalization via the trace dual

This file develops the trace-dual argument which avoids factoriality and normality assumptions on the base. For a finite separable extension L / K and the finite normalization B of a Noetherian domain A, the trace dual of B is a nonzero finite B-module. Its double trace dual is B, by the determinant trick and integral closedness of B inside L. A regular pair on A can then test membership in that double trace dual.

Imports6
  • Mathlib.Algebra.Module.LocalizedModule.Int
  • Mathlib.RingTheory.DedekindDomain.Different
  • Mathlib.RingTheory.DedekindDomain.IntegralClosure
  • Mathlib.RingTheory.Finiteness.Basic
  • Mathlib.RingTheory.Noetherian.Basic
  • Mathlib.RingTheory.Regular.RegularSequence
Imported by2

Declarations

theorem

traceDual_one_finite

L54 ↗
EtaleFundamentalGroups.traceDual_one_finite
Documentation

The trace dual of a finite normalization is finite over the normalization.

The key point is that the trace pairing embeds it into the A-dual of B. That dual is finite because A is Noetherian, and restriction of scalars then gives finite generation over B.

Source context 16 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped Pointwise
open Module
open nonZeroDivisors
open RingTheory.Sequence
universe u v w
section TraceDualFinite
variable {A : Type u} {K : Type v} {L : Type w}
variable [CommRing A] [hA_domain : IsDomain A] [hA_noetherian : IsNoetherianRing A]
variable [hK_field : Field K] [hAK : Algebra A K] [hfrac : IsFractionRing A K]
variable [Field L] [Algebra A L] [hKL : Algebra K L] [hAKL : IsScalarTower A K L]
variable [hfiniteDimensional : FiniteDimensional K L]
variable [hseparable : Algebra.IsSeparable K L]
variable [hBfinite : Module.Finite A (integralClosure A L)]
local notation "B" => integralClosure A L
Lean source · statement
theorem traceDual_one_finite :
    Module.Finite B (Submodule.traceDual A K (1 : Submodule B L))
theorem

traceDual_one_ne_bot

L110 ↗
EtaleFundamentalGroups.traceDual_one_ne_bot
Documentation

The trace dual of a finite normalization is nonzero.

Choose finitely many A-module generators of B and clear the denominators of their traces simultaneously. The resulting nonzero element of A lies in the trace dual by linearity.

Source context 17 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped Pointwise
open Module
open nonZeroDivisors
open RingTheory.Sequence
universe u v w
section TraceDualFinite
variable {A : Type u} {K : Type v} {L : Type w}
variable [CommRing A] [hA_domain : IsDomain A] [hA_noetherian : IsNoetherianRing A]
variable [hK_field : Field K] [hAK : Algebra A K] [hfrac : IsFractionRing A K]
variable [Field L] [Algebra A L] [hKL : Algebra K L] [hAKL : IsScalarTower A K L]
variable [hfiniteDimensional : FiniteDimensional K L]
variable [hseparable : Algebra.IsSeparable K L]
variable [hBfinite : Module.Finite A (integralClosure A L)]
local notation "B" => integralClosure A L
omit [IsNoetherianRing A] [FiniteDimensional K L] [Algebra.IsSeparable K L] in
Lean source · statement
theorem traceDual_one_ne_bot :
    Submodule.traceDual A K (1 : Submodule B L) ≠ ⊥
theorem

traceDual_traceDual_one_eq_one_of_finite

L180 ↗
EtaleFundamentalGroups.traceDual_traceDual_one_eq_one_of_finite
Documentation

The double trace dual of a finite normalization is the normalization.

For I = Bᵛ, an element of Iᵛ stabilizes I: this follows by moving the extra factor across the commutative trace pairing. Since I is nonzero and finite, the determinant trick makes that element integral over B; the integral closedness of B inside L then puts it back in B.

Source context 16 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped Pointwise
open Module
open nonZeroDivisors
open RingTheory.Sequence
universe u v w
section TraceDualFinite
variable {A : Type u} {K : Type v} {L : Type w}
variable [CommRing A] [hA_domain : IsDomain A] [hA_noetherian : IsNoetherianRing A]
variable [hK_field : Field K] [hAK : Algebra A K] [hfrac : IsFractionRing A K]
variable [Field L] [Algebra A L] [hKL : Algebra K L] [hAKL : IsScalarTower A K L]
variable [hfiniteDimensional : FiniteDimensional K L]
variable [hseparable : Algebra.IsSeparable K L]
variable [hBfinite : Module.Finite A (integralClosure A L)]
local notation "B" => integralClosure A L
Lean source · statement
theorem traceDual_traceDual_one_eq_one_of_finite :
    Submodule.traceDual A K
      (Submodule.traceDual A K (1 : Submodule B L)) = 1
theorem

exists_integralClosure_factor_of_mul_eq_mul_of_isRegular

L214 ↗
EtaleFundamentalGroups.exists_integralClosure_factor_of_mul_eq_mul_of_isRegular
Documentation

A regular pair on a Noetherian domain remains a divisibility test on its finite normalization in a finite separable field extension.

Concretely, if y * b = x * c in the normalization and [x, y] is regular on A, then x divides b in the normalization. This proof uses neither a UFD instance, integral closedness of A, nor primality of x.

Source context 17 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped Pointwise
open Module
open nonZeroDivisors
open RingTheory.Sequence
universe u v w
section TraceDualFinite
variable {A : Type u} {K : Type v} {L : Type w}
variable [CommRing A] [hA_domain : IsDomain A] [hA_noetherian : IsNoetherianRing A]
variable [hK_field : Field K] [hAK : Algebra A K] [hfrac : IsFractionRing A K]
variable [Field L] [Algebra A L] [hKL : Algebra K L] [hAKL : IsScalarTower A K L]
variable [hfiniteDimensional : FiniteDimensional K L]
variable [hseparable : Algebra.IsSeparable K L]
variable [hBfinite : Module.Finite A (integralClosure A L)]
local notation "B" => integralClosure A L
include K hA_domain hA_noetherian hK_field hAK hfrac hKL hAKL
  hfiniteDimensional hseparable hBfinite in
Lean source · statement
theorem exists_integralClosure_factor_of_mul_eq_mul_of_isRegular
    {x y : A} (hregular : IsRegular A [x, y])
    {b c : B}
    (hbc : algebraMap A B y * b = algebraMap A B x * c) :
    ∃ d : B, b = algebraMap A B x * d

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