Norm and trace of algebras

TheoremThe norm commutes with base change#✓fully proved

Let \(A\), \(A'\) and \(B\) be commutative rings, where \(A'\) and \(B\) are \(A\)-algebras and \(B\) is a free \(A\)-module of finite rank. Then for every \(b \in B\), the image of the norm \(N_{B/A}(b)\) under the structure map \(A \to A'\) equals the norm \(N_{(A' \otimes_A B)/A'}(1 \otimes b)\) of \(1 \otimes b\) in the \(A'\)-algebra \(A' \otimes_A B\).

theorem norm_baseChange (b : B) :
    algebraMap A A' (norm A b) =
      norm A' ((TensorProduct.includeRight b : A' ⊗[A] B))

Sources

ATLAS NumberTheoryI, Lemma 4.49 (norm clause).

TheoremThe trace commutes with base change#✓fully proved

Let \(A\), \(A'\) and \(B\) be commutative rings, where \(A'\) and \(B\) are \(A\)-algebras and \(B\) is a free \(A\)-module of finite rank. Then for every \(b \in B\), the image of the trace \(T_{B/A}(b)\) under the structure map \(A \to A'\) equals the trace \(T_{(A' \otimes_A B)/A'}(1 \otimes b)\) of \(1 \otimes b\) in the \(A'\)-algebra \(A' \otimes_A B\).

theorem trace_baseChange (b : B) :
    algebraMap A A' (trace A B b) =
      trace A' (A' ⊗[A] B) (TensorProduct.includeRight b)

Sources

ATLAS NumberTheoryI, Lemma 4.49 (trace clause).

TheoremNorm in a product algebra is the product of norms#✓fully proved

The norm of a product algebra is the product of the norms of the components: left multiplication by (x₁, x₂) is the product map of the left multiplications, and the determinant of a product map is the product of the determinants.

theorem Algebra.norm_prod {R A B : Type*} [CommRing R] [Ring A] [Ring B]
    [Algebra R A] [Algebra R B] [Module.Free R A] [Module.Finite R A]
    [Module.Free R B] [Module.Finite R B] (x : A × B) :
    Algebra.norm R x = Algebra.norm R x.1 * Algebra.norm R x.2

TheoremNorm on a subsingleton algebra is one#✓fully proved

The norm on a subsingleton algebra is 1: left multiplication by any element is the identity map on a subsingleton module, hence has determinant 1.

theorem Algebra.norm_of_subsingleton {R A : Type*} [CommRing R] [Ring A]
    [Algebra R A] [Subsingleton A] (a : A) : Algebra.norm R a = 1

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.