Documentation

TauCeti.RingTheory.Norm.Projective

The norm of a finite locally free algebra #

Let S be an R-algebra which is finite projective as an R-module, that is, finite locally free over R. Mathlib's Algebra.norm R is the determinant of multiplication when S has a finite basis over R, and is 1 otherwise. This file defines the norm Algebra.projectiveNorm R : S →* R as the determinant LinearMap.projectiveDet of multiplication, which is defined for every finite projective module. It agrees with Algebra.norm R when S is free (Algebra.projectiveNorm_eq_norm), commutes with arbitrary base change (Algebra.projectiveNorm_baseChange_tmul), is invariant under isomorphisms of algebras, and detects units.

Geometrically, for a finite locally free morphism Spec S ⟶ Spec R, this is the norm Norm_{S/R} : S → R of functions, whose compatibility with base change is the compatibility of the norm with pullback along every Spec A ⟶ Spec R. Full sets of sections of a finite locally free scheme over a base are defined by an identity between this norm and a product of values of sections, required after every base change (Katz–Mazur, Arithmetic Moduli of Elliptic Curves, 1.8).

Main definitions #

Main results #

References #

source
noncomputable def Algebra.projectiveNorm (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S] [Module.Projective R S] :
S →* R

The norm of an element x of an R-algebra S which is finite projective as an R-module: the determinant LinearMap.projectiveDet of multiplication by x. It is Algebra.norm R x when S is free over R (projectiveNorm_eq_norm).

Instances For
    source
    theorem Algebra.projectiveNorm_apply (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S] [Module.Projective R S] (x : S) :
    (projectiveNorm R) x = LinearMap.projectiveDet ((lmul R S) x)
    source
    @[simp]
    theorem Algebra.projectiveNorm_baseChange_tmul {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S] [Module.Projective R S] (A : Type u_3) [CommRing A] [Algebra R A] (x : S) :
    (projectiveNorm A) (1 ⊗ₜ[R] x) = (algebraMap R A) ((projectiveNorm R) x)

    The norm of a finite projective algebra commutes with base change: the norm of 1 ⊗ x in A ⊗[R] S over A is the image in A of the norm of x over R.

    source
    theorem Algebra.projectiveNorm_eq_of_algEquiv {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S] [Module.Projective R S] {T : Type u_3} [Ring T] [Algebra R T] [Module.Finite R T] [Module.Projective R T] (e : S ≃ₐ[R] T) (x : S) :
    (projectiveNorm R) (e x) = (projectiveNorm R) x

    The norm of a finite projective algebra is invariant under isomorphisms of algebras.

    source
    @[simp]
    theorem Algebra.isUnit_projectiveNorm_iff {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S] [Module.Projective R S] {x : S} :
    IsUnit ((projectiveNorm R) x) ↔ IsUnit x

    An element of a finite projective algebra is a unit if and only if its norm is a unit.

    source
    theorem Algebra.projectiveNorm_eq_norm (R : Type u_1) {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S] [Module.Free R S] (x : S) :
    (projectiveNorm R) x = (norm R) x

    For an algebra which is free of finite rank, projectiveNorm is the norm Algebra.norm.

    Use this comparison explicitly: automatic rewriting to norm would hide the unit-detection and base-change simplification rules for projectiveNorm.

    source
    theorem Algebra.projectiveNorm_rTensor {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] [Module.Finite R S] [Module.Projective R S] {A : Type u_3} {A' : Type u_4} [CommRing A] [Algebra R A] [CommRing A'] [Algebra R A'] (φ : A →ₐ[R] A') (x : TensorProduct R A S) :
    (projectiveNorm A') ((TensorProduct.rTensor S φ) x) = φ ((projectiveNorm A) x)

    The norm of a finite projective algebra commutes with base change along an R-algebra map φ : A →ₐ[R] A': the norm over A' of the image of x ∈ A ⊗[R] S in A' ⊗[R] S is the image under φ of the norm of x over A.

    source
    theorem Algebra.projectiveNorm_mem_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S] [Module.Projective R S] {p : Ideal R} [p.IsPrime] {x : S} :
    (projectiveNorm R) x ∈ p ↔ ∃ P ∈ p.primesOver S, x ∈ P

    The norm of x lies in a prime p of R if and only if x lies in some prime of S over p: geometrically, the zero locus of Norm_{S/R}(x) on Spec R is the image of the zero locus of x on Spec S.

    source
    theorem LinearMap.projectiveDet_restrictScalars {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] {M : Type u_3} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] [Module.Finite S M] [Module.Projective S M] [Module.Finite R M] [Module.Projective R M] (f : Module.End S M) :
    projectiveDet (↑R f) = (Algebra.norm R) (projectiveDet f)

    Transitivity of the determinant for a finite projective module over a finite free algebra: if S is finite free over R and M is a finite projective S-module, the determinant over R of an S-linear endomorphism f of M is the norm from S to R of its determinant over S. This extends Mathlib's LinearMap.det_restrictScalars, where M is free over S.

    source
    theorem Algebra.norm_projectiveNorm {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] {C : Type u_3} [Ring C] [Algebra R C] [Algebra S C] [IsScalarTower R S C] [Module.Finite S C] [Module.Projective S C] [Module.Finite R C] [Module.Projective R C] (c : C) :
    (norm R) ((projectiveNorm S) c) = (projectiveNorm R) c

    Transitivity of the norm for a finite projective algebra over a finite free algebra: if S is finite free over R and C is a finite projective S-algebra, then Norm_{S/R} ∘ Norm_{C/S} = Norm_{C/R}. This extends Mathlib's Algebra.norm_norm, where C is free over S.