The trace modulo an ideal

Let S be a finite free R-algebra and I an ideal of R. The trace of S ⧸ IS over R ⧸ I of the class of x is the class of the trace of x. Mathlib's Algebra.trace_quotient_mk is the case where R is local and I is its maximal ideal; here I is arbitrary, which is what a computation of the trace modulo a power 𝔪 ^ n of a maximal ideal needs. It is the trace counterpart of TauCeti.Algebra.norm_quotient_mk.

It also computes the trace modulo I of an element whose multiplication maps S ⧸ IS into a free submodule with a known basis, such as a summand of S ⧸ IS through which it acts, which is how the trace of a finite extension of function fields is computed locally at one place.

Main results

• TauCeti.Algebra.trace_quotient_map_mk: the trace of S ⧸ IS over R ⧸ I of the class of x is the class of the trace of x.
• TauCeti.Algebra.trace_sub_sum_mem_of_forall_mul_sub_sum_mem: if, modulo IS, multiplication by z maps into the span of linearly independent b j and acts on them by the matrix a, then Tr_{S/R} z ≡ ∑ j, a j j modulo I.
• TauCeti.Algebra.trace_sub_one_mem_of_mul_self_sub_mem: its rank-one case, an idempotent of rank one modulo I has trace 1 modulo I.

@[simp]

theorem TauCeti.Algebra.trace_quotient_map_mk {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] (I : Ideal R) (x : S) : (Algebra.trace (R ⧸ I) (S ⧸ Ideal.map (algebraMap R S) I)) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) I)) x) = (Ideal.Quotient.mk I) ((Algebra.trace R S) x)

The trace commutes with reduction modulo an ideal. For a finite free algebra S over R and an ideal I of R, the trace of S ⧸ IS over R ⧸ I of the class of x is the class of the trace of x.

theorem TauCeti.Algebra.trace_mem_of_mem_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] {I : Ideal R} {x : S} (hx : x ∈ Ideal.map (algebraMap R S) I) : (Algebra.trace R S) x ∈ I

The trace of an element of IS lies in I.

theorem TauCeti.Algebra.trace_sub_sum_mem_of_forall_mul_sub_sum_mem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] {ι : Type u_3} [Fintype ι] {I : Ideal R} {z : S} {b : ι → S} {a : ι → ι → R} (hspan : ∀ (s : S), ∃ (c : ι → R), z * s - ∑ j : ι, (algebraMap R S) (c j) * b j ∈ Ideal.map (algebraMap R S) I) (hindep : ∀ (c : ι → R), ∑ j : ι, (algebraMap R S) (c j) * b j ∈ Ideal.map (algebraMap R S) I → ∀ (j : ι), c j ∈ I) (hzb : ∀ (j : ι), z * b j - ∑ l : ι, (algebraMap R S) (a j l) * b l ∈ Ideal.map (algebraMap R S) I) : (Algebra.trace R S) z - ∑ j : ι, a j j ∈ I

The trace on a free submodule with a known basis, modulo an ideal. Let J = IS. Suppose that modulo J, multiplication by z maps S into the span of the b j, that the b j are linearly independent over R ⧸ I, and that z acts on them by the matrix a: every z * s is congruent to some ∑ c j * b j, ∑ c j * b j ∈ J only when every c j ∈ I, and z * b j ≡ ∑ l, a j l * b l. Then Tr_{S/R} z ≡ ∑ j, a j j modulo I.

Modulo J, the class of z maps S ⧸ J into the submodule spanned by the classes of the b j, which is free with that basis, so its trace is the trace of the matrix a. No hypothesis on R ⧸ I is needed: the basis of that submodule is given. Typically z acts through a projection w onto a summand of S ⧸ J, that is z * w ≡ z, and every w * s lies in the span of the b j.

theorem TauCeti.Algebra.trace_sub_one_mem_of_mul_self_sub_mem {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] [Module.Free R S] [Module.Finite R S] {I : Ideal R} {w : S} (hw : w * w - w ∈ Ideal.map (algebraMap R S) I) (hspan : ∀ (b : S), ∃ (c : R), w * b - (algebraMap R S) c * w ∈ Ideal.map (algebraMap R S) I) (hinj : ∀ (c : R), (algebraMap R S) c * w ∈ Ideal.map (algebraMap R S) I → c ∈ I) : (Algebra.trace R S) w - 1 ∈ I

An idempotent of rank one modulo an ideal has trace one. Suppose the class of w in S ⧸ IS is idempotent, and that the ideal it generates is free of rank one over R ⧸ I with basis that class: every w * b is congruent to some c * w with c ∈ R, and c * w ∈ IS only for c ∈ I. Then Tr_{S/R} w ≡ 1 modulo I.

This is the rank-one case of TauCeti.Algebra.trace_sub_sum_mem_of_forall_mul_sub_sum_mem for z = w, with the single basis vector w on which w acts by 1.