Module

TensorNormBaseChange.lean

Nyll.ClassFieldTheory.Theorems.NormTheorems.TensorNormBaseChange

1 declaration indexed from sourceView source ↗

Module documentation

Determinant norm and scalar extension

For a finite field extension L / K, the norm of y : L is unchanged by base change, in the sense that the determinant norm of 1 ⊗ y over a commutative K-algebra A is the image of its field norm over K. This applies to the whole tensor algebra, whether or not it is a field.

Imports2

Mathlib.RingTheory.Norm.Basic
Mathlib.RingTheory.TensorProduct.Basic

Imported by2

theorem

tensorNorm_includeRight

L28 ↗

ClassFieldTheory.tensorNorm_includeRight

Documentation

The determinant norm on A ⊗[K] L of a globally defined element is the base change of its field norm. In particular, no Galois assumption or choice of a factor of the tensor algebra is required.

Source context 3 commands

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

open scoped TensorProduct
namespace ClassFieldTheory
universe u v w

Lean source · statement

theorem tensorNorm_includeRight
    (K : Type u) (L : Type v) (A : Type w)
    [Field K] [Field L] [Algebra K L] [FiniteDimensional K L]
    [CommRing A] [Algebra K A] [Nontrivial A]
    (y : L) :
    Algebra.norm A
        (Algebra.TensorProduct.includeRight (R := K) (A := A) (B := L) y) =
      algebraMap K A (Algebra.norm K y)

Module documentation

Determinant norm and scalar extension

Declarations

tensorNorm_includeRight