Module

FiniteFreeDiscriminant.lean

Nyll.SchemeTheory.RingTheory.Ramification.Trace.FiniteFreeDiscriminant

6 declarations indexed from sourceView source ↗

Module documentation

Trace discriminants of finite free algebras

This file develops the linear-algebra input for the dimension-two branch-locus argument. For a finite free commutative algebra, the trace pairing is onto the module dual exactly when the discriminant of a basis is a unit. The statement works over an arbitrary commutative base ring; no domain, locality, or etaleness hypothesis is used.

Imports7

Mathlib.RingTheory.Discriminant
Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Mathlib.RingTheory.Smooth.Fiber
Mathlib.RingTheory.Unramified.Finite
Mathlib.LinearAlgebra.TensorProduct.Basis
Mathlib.LinearAlgebra.FreeModule.Finite.Basic
Mathlib.Data.Fintype.EquivFin

Imported by2

theorem

traceForm_surjective_iff_isUnit_discr

L35 ↗

EtaleFundamentalGroups.traceForm_surjective_iff_isUnit_discr

Documentation

For a finite basis, surjectivity of the trace-pairing map is equivalent to the discriminant being a unit.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Module
open scoped TensorProduct
universe u v w

Lean source · statement

theorem traceForm_surjective_iff_isUnit_discr
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [CommRing S] [Algebra R S]
    [Fintype ι] [DecidableEq ι]
    (b : Basis ι R S) :
    Function.Surjective (Algebra.traceForm R S) ↔
      IsUnit (Algebra.discr R b)

theorem

traceForm_injective_of_isUnit_discr

L87 ↗

EtaleFundamentalGroups.traceForm_injective_of_isUnit_discr

Documentation

A unit trace discriminant makes the trace-pairing map injective. This direction works over an arbitrary commutative base because the corresponding trace matrix is invertible.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Module
open scoped TensorProduct
universe u v w

Lean source · statement

theorem traceForm_injective_of_isUnit_discr
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [CommRing S] [Algebra R S]
    [Fintype ι] [DecidableEq ι]
    (b : Basis ι R S) (hdisc : IsUnit (Algebra.discr R b)) :
    Function.Injective (Algebra.traceForm R S)

theorem

traceForm_surjective_of_formallyUnramified

L120 ↗

EtaleFundamentalGroups.traceForm_surjective_of_formallyUnramified

Documentation

For a finite free algebra, formal unramifiedness makes the trace-pairing map onto the module dual. The preimage of a functional is obtained by contracting that functional with the separability element.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Module
open scoped TensorProduct
universe u v w

Lean source · statement

theorem traceForm_surjective_of_formallyUnramified
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [CommRing S] [Algebra R S]
    [_root_.Finite ι]
    (b : Basis ι R S) (h : Algebra.FormallyUnramified R S) :
    Function.Surjective (Algebra.traceForm R S)

theorem

formallyUnramified_of_traceForm_surjective

L193 ↗

EtaleFundamentalGroups.formallyUnramified_of_traceForm_surjective

Documentation

Surjectivity of the trace pairing produces the separability element witnessing formal unramifiedness. The element is the Casimir tensor associated to a basis and its trace-dual family; both its multiplication and centrality identities are proved from the trace pairing.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Module
open scoped TensorProduct
universe u v w

Lean source · statement

theorem formallyUnramified_of_traceForm_surjective
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [CommRing S] [Algebra R S]
    [_root_.Finite ι]
    (b : Basis ι R S)
    (hsurj : Function.Surjective (Algebra.traceForm R S)) :
    Algebra.FormallyUnramified R S

theorem

formallyUnramified_iff_isUnit_discr

L262 ↗

EtaleFundamentalGroups.formallyUnramified_iff_isUnit_discr

Documentation

A finite free commutative algebra is formally unramified exactly when the discriminant of one (equivalently, every) basis is a unit.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Module
open scoped TensorProduct
universe u v w

Lean source · statement

theorem formallyUnramified_iff_isUnit_discr
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [CommRing S] [Algebra R S]
    [Fintype ι] [DecidableEq ι]
    (b : Basis ι R S) :
    Algebra.FormallyUnramified R S ↔ IsUnit (Algebra.discr R b)

theorem

etale_iff_isUnit_discr

L278 ↗

EtaleFundamentalGroups.etale_iff_isUnit_discr

Documentation

A finite free commutative algebra is étale exactly when the discriminant of a basis is a unit. Finite presentation and flatness are supplied by the same finite basis.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open Module
open scoped TensorProduct
universe u v w

Lean source · statement

theorem etale_iff_isUnit_discr
    {R : Type u} {S : Type v} {ι : Type w}
    [CommRing R] [CommRing S] [Algebra R S]
    [Fintype ι] [DecidableEq ι]
    (b : Basis ι R S) :
    Algebra.Etale R S ↔ IsUnit (Algebra.discr R b)

Module documentation

Trace discriminants of finite free algebras

Declarations

traceForm_surjective_iff_isUnit_discr

traceForm_injective_of_isUnit_discr

traceForm_surjective_of_formallyUnramified

formallyUnramified_of_traceForm_surjective

formallyUnramified_iff_isUnit_discr

etale_iff_isUnit_discr