Norms and traces of finite products

This file records the determinant, norm, and trace calculations for finite dependent products. TauCeti.Algebra.normUnits_eq_finprod_of_algEquiv transports the unit norm to a finite product; TauCeti.Algebra.mem_range_normUnits_iff_of_algEquiv characterizes its range. The scalar-extension identities used by the number-field local-global development live in TauCeti.RingTheory.NormTrace.BaseChange.

@[simp]

theorem TauCeti.Algebra.norm_pi {K : Type u} [CommRing K] {ι : Type v} [Fintype ι] {L : ι → Type u_1} [(i : ι) → Ring (L i)] [(i : ι) → Algebra K (L i)] [∀ (i : ι), Module.Free K (L i)] [∀ (i : ι), Module.Finite K (L i)] (x : (i : ι) → L i) : (Algebra.norm K) x = ∏ i : ι, (Algebra.norm K) (x i)

The norm of an element of a finite dependent product is the product of its component norms.

theorem TauCeti.Algebra.normUnits_eq_finprod_of_algEquiv {K : Type u} [CommRing K] {ι : Type u_1} [Finite ι] {S : Type u_2} [Ring S] [Algebra K S] {T : ι → Type u_3} [(i : ι) → Ring (T i)] [(i : ι) → Algebra K (T i)] [∀ (i : ι), Module.Free K (T i)] [∀ (i : ι), Module.Finite K (T i)] (e : S ≃ₐ[K] (i : ι) → T i) (u : Sˣ) : (normUnits K) u = ∏ᶠ (i : ι), (normUnits K) (MulEquiv.piUnits ((Units.map e.toMulEquiv.toMonoidHom) u) i)

Transporting a norm on units to a finite product gives the product of the component norms.

theorem TauCeti.Algebra.mem_range_normUnits_iff_of_algEquiv {K : Type u} [CommRing K] {ι : Type u_1} [Finite ι] {S : Type u_2} [Ring S] [Algebra K S] {T : ι → Type u_3} [(i : ι) → Ring (T i)] [(i : ι) → Algebra K (T i)] [∀ (i : ι), Module.Free K (T i)] [∀ (i : ι), Module.Finite K (T i)] (e : S ≃ₐ[K] (i : ι) → T i) (a : Kˣ) : a ∈ (normUnits K).range ↔ ∃ (u : (i : ι) → (T i)ˣ), ∏ᶠ (i : ι), (normUnits K) (u i) = a

A unit lies in the norm range of an algebra equivalent to a finite product exactly when it is a product of norms of units of the factors.

@[simp]

theorem TauCeti.Algebra.trace_pi {K : Type u} [CommRing K] {ι : Type v} [Fintype ι] {L : ι → Type u_1} [(i : ι) → CommRing (L i)] [(i : ι) → Algebra K (L i)] [∀ (i : ι), Module.Free K (L i)] [∀ (i : ι), Module.Finite K (L i)] (x : (i : ι) → L i) : (Algebra.trace K ((i : ι) → L i)) x = ∑ i : ι, (Algebra.trace K (L i)) (x i)

The trace of an element of a finite dependent product is the sum of its component traces.