Étale algebras and the trace form

TheoremÉtale criterion via semisimple base change#✓fully proved

Let \(K\) be a field, \(\Omega\) an algebraically closed field extension of \(K\), and \(A\) a commutative \(K\)-algebra that is finite-dimensional over \(K\). If the ring \(\Omega \otimes_K A\) is semisimple, then \(A\) is étale over \(K\).

theorem Algebra.Etale.of_isSemisimpleRing_tensorProduct
    {K Ω A : Type*} [Field K] [Field Ω] [Algebra K Ω] [IsAlgClosed Ω]
    [CommRing A] [Algebra K A] [Module.Finite K A]
    (h : IsSemisimpleRing (Ω ⊗[K] A)) : Algebra.Etale K A

TheoremTrace on a finite product of algebras#✓fully proved

Let \(K\) be a field, and for a finite-dimensional commutative \(K\)-algebra \(A\) and \(z \in A\) write \(\operatorname{Tr}_{A/K}(z)\) for the trace of the \(K\)-linear map given by multiplication by \(z\). Let \((A_i)_{i \in I}\) be a family of finite-dimensional commutative \(K\)-algebras indexed by a finite set \(I\), and let \(P = \prod_{i \in I} A_i\). Then for every \(x = (x_i)_{i \in I}\) in \(P\), \(\operatorname{Tr}_{P/K}(x) = \sum_{i \in I} \operatorname{Tr}_{A_i/K}(x_i)\).

theorem trace_pi {ι : Type*} [Fintype ι] {A : ι → Type*}
    [∀ i, CommRing (A i)] [∀ i, Algebra K (A i)]
    [∀ i, Module.Finite K (A i)] [∀ i, Module.Free K (A i)]
    (x : ∀ i, A i) :
    trace K (∀ i, A i) x = ∑ i, trace K (A i) (x i)
Used by 1
Used byTrace form of a finite product of algebras

TheoremTrace form of a finite product of algebras#✓fully proved

Let \(K\) be a field, and for a finite-dimensional commutative \(K\)-algebra \(A\) and \(z \in A\) write \(\operatorname{Tr}_{A/K}(z)\) for the trace of the \(K\)-linear map given by multiplication by \(z\). Let \((A_i)_{i \in I}\) be a family of finite-dimensional commutative \(K\)-algebras indexed by a finite set \(I\), and let \(P = \prod_{i \in I} A_i\). Then for all \(x = (x_i)_{i \in I}\) and \(y = (y_i)_{i \in I}\) in \(P\), \(\operatorname{Tr}_{P/K}(xy) = \sum_{i \in I} \operatorname{Tr}_{A_i/K}(x_i y_i)\), that is, the trace form of \(P\) over \(K\) is the sum of the trace forms of the factors.

theorem traceForm_pi {ι : Type*} [Fintype ι] {A : ι → Type*}
    [∀ i, CommRing (A i)] [∀ i, Algebra K (A i)]
    [∀ i, Module.Finite K (A i)] [∀ i, Module.Free K (A i)]
    (x y : ∀ i, A i) :
    traceForm K (∀ i, A i) x y
      = ∑ i, traceForm K (A i) (x i) (y i)
Uses 1 · Used by 1
Proof usesTrace on a finite product of algebras
Used byTrace form criterion for étale algebras

TheoremThe trace form is invariant under algebra isomorphisms#✓fully proved

For a commutative algebra \(A\) over a field \(K\) and \(z \in A\), write \(\operatorname{Tr}_{A/K}(z)\) for the trace of the \(K\)-linear map given by multiplication by \(z\), taken to be \(0\) when \(A\) is infinite-dimensional over \(K\). Let \(R\) and \(S\) be commutative algebras over \(K\) and let \(e : R \to S\) be an isomorphism of \(K\)-algebras. Then for all \(x, y \in R\) we have \(\operatorname{Tr}_{S/K}(e(x)\,e(y)) = \operatorname{Tr}_{R/K}(xy)\), that is, \(e\) carries the trace form of \(R\) over \(K\) to the trace form of \(S\) over \(K\).

theorem traceForm_apply_of_algEquiv {R S : Type*} [CommRing R] [CommRing S]
    [Algebra K R] [Algebra K S] (e : R ≃ₐ[K] S) (x y : R) :
    traceForm K S (e x) (e y) = traceForm K R x y
Used by 1
Used byTrace form criterion for étale algebras

TheoremNilpotent elements pair to zero under the trace form#✓fully proved

Let \(R\) be a commutative algebra over a field \(K\), and for \(z \in R\) write \(\operatorname{Tr}_{R/K}(z)\) for the trace of the \(K\)-linear map given by multiplication by \(z\), taken to be \(0\) when \(R\) is infinite-dimensional over \(K\). If \(x, y \in R\) and \(x\) is nilpotent, then the trace form of \(R\) over \(K\) vanishes at \((x, y)\), that is, \(\operatorname{Tr}_{R/K}(xy) = 0\).

Multiplication by a nilpotent element is a nilpotent endomorphism, whose trace vanishes.

theorem traceForm_apply_eq_zero_of_isNilpotent {R : Type*} [CommRing R]
    [Algebra K R] {x y : R} (hx : IsNilpotent x) :
    traceForm K R x y = 0
Used by 1
Used byA nondegenerate trace form forces the algebra to be reduced

TheoremA nondegenerate trace form forces the algebra to be reduced#✓fully proved

Let \(R\) be a commutative algebra over a field \(K\). For \(z \in R\) write \(\operatorname{Tr}_{R/K}(z)\) for the trace of the \(K\)-linear map given by multiplication by \(z\), taken to be \(0\) when \(R\) is infinite-dimensional over \(K\). If the trace form \((x, y) \mapsto \operatorname{Tr}_{R/K}(xy)\) of \(R\) over \(K\) is nondegenerate, then \(R\) is reduced, that is, its only nilpotent element is \(0\).

Every nilpotent element lies in the kernel of the trace form, hence is zero.

theorem isReduced_of_traceForm_nondegenerate {R : Type*} [CommRing R]
    [Algebra K R] (h : (traceForm K R).Nondegenerate) : IsReduced R
Uses 1 · Used by 1
Proof usesNilpotent elements pair to zero under the trace form
Used byTrace form criterion for étale algebras

TheoremTrace form criterion for étale algebras#✓fully proved

Let \(R\) be a finite-dimensional commutative algebra over a field \(K\), and for \(z \in R\) write \(\operatorname{Tr}_{R/K}(z)\) for the trace of the \(K\)-linear map given by multiplication by \(z\). Then the trace form \((x, y) \mapsto \operatorname{Tr}_{R/K}(xy)\) of \(R\) over \(K\) is nondegenerate if and only if \(R\) is étale over \(K\).

theorem traceForm_nondegenerate_iff_etale {R : Type u} [CommRing R] [Algebra K R]
    [Module.Finite K R] :
    (traceForm K R).Nondegenerate ↔ Etale K R
Sources
  • ATLAS NumberTheoryI Theorem 5.20.
Uses 3 · Used by 1
Proof usesA nondegenerate trace form forces the algebra to be reduced · The trace form is invariant under algebra isomorphisms · Trace form of a finite product of algebras
Used byÉtale algebras are detected by the discriminant

TheoremDiscriminant and nondegeneracy of the trace form#✓fully proved

Let \(R\) be a commutative algebra over a field \(K\) and let \(b\) be a \(K\)-basis of \(R\) indexed by a finite set. For \(z \in R\) write \(\operatorname{Tr}_{R/K}(z)\) for the trace of the \(K\)-linear map given by multiplication by \(z\). Then the discriminant of \(b\) over \(K\) is nonzero if and only if the trace form \((x, y) \mapsto \operatorname{Tr}_{R/K}(xy)\) of \(R\) over \(K\) is nondegenerate.

theorem discr_ne_zero_iff_traceForm_nondegenerate {R : Type*} [CommRing R]
    [Algebra K R] {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K R) :
    Algebra.discr K b ≠ 0 ↔ (traceForm K R).Nondegenerate
Used by 1
Used byÉtale algebras are detected by the discriminant

TheoremÉtale algebras are detected by the discriminant#✓fully proved

Let \(R\) be a commutative algebra over a field \(K\) and let \(b\) be a \(K\)-basis of \(R\) indexed by a finite set. Then the discriminant of \(b\) over \(K\) is nonzero if and only if \(R\) is étale over \(K\).

theorem discr_ne_zero_iff_etale {R : Type u} [CommRing R] [Algebra K R]
    {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K R) :
    Algebra.discr K b ≠ 0 ↔ Etale K R
Sources
  • ATLAS NumberTheoryI Lemma 12.18.
Uses 2 · Used by 2
Proof usesDiscriminant and nondegeneracy of the trace form · Trace form criterion for étale algebras
Used byÉtale algebras have nonzero discriminant · A nonzero discriminant forces étaleness

TheoremÉtale algebras have nonzero discriminant#✓fully proved

Let \(R\) be a commutative algebra over a field \(K\) that is étale over \(K\). Then for every \(K\)-basis \(b\) of \(R\) indexed by a finite set, the discriminant of \(b\) over \(K\) is nonzero.

theorem discr_ne_zero_of_etale {R : Type u} [CommRing R] [Algebra K R]
    {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K R)
    (hR : Etale K R) :
    Algebra.discr K b ≠ 0
Sources
  • ATLAS NumberTheoryI Lemma 12.18, one direction.
Uses 1
Proof usesÉtale algebras are detected by the discriminant

TheoremA nonzero discriminant forces étaleness#✓fully proved

Let \(R\) be a commutative algebra over a field \(K\) and let \(b\) be a \(K\)-basis of \(R\) indexed by a finite set. If the discriminant of \(b\) over \(K\) is nonzero, then \(R\) is étale over \(K\).

theorem etale_of_discr_ne_zero {R : Type u} [CommRing R] [Algebra K R]
    {ι : Type*} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K R)
    (h : Algebra.discr K b ≠ 0) :
    Etale K R
Sources
  • ATLAS NumberTheoryI Lemma 12.18, one direction.
Uses 1
Proof usesÉtale algebras are detected by the discriminant
11 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.