Projective conic algebras: the trace defect vanishes (GPR 16.7, GPR 16.14(b))

For an alternative conic algebra whose underlying module is finitely generated projective, the conjugation is an algebra anti-homomorphism. Conic/Basic.lean proves this over a field, and Conic/TraceDefectCounterexample.lean shows it is false over an arbitrary base; projectivity is exactly what separates the two.

The argument

ConicAlgebra.traceDefect_smul_eq_smul_one (alternativity) gives, for every x,

d(x, y) • x = μ(x, y) • 1, where d is the trace defect.

Two facts turn this into d = 0.

• 1 is unimodular (GPR 16.7, via GPR 11.15). Over a projective module a quadratic form is b(x, x) for some bilinear b (QuadraticMap.bilinRepr), and then λ := b(1, ·) has λ 1 = n 1 = 1. Applying λ to the displayed identity evaluates μ(x, y) = d(x, y) λ(x), so

  d(x, y) • (x - λ(x) • 1) = 0.

  In other words d(·, y) annihilates its own argument on N := ker λ.

• A self-annihilating functional on a finitely generated projective module vanishes (LinearMap.eq_zero_of_smul_self_eq_zero, Module/SelfAnnihilating.lean). N is a direct summand of A, hence finitely generated projective, so d(·, y) vanishes on N; and A is k · 1 + N with d(1, y) = 0, so d vanishes identically.

This is GPR 16.14(b) — flexibility plus projectivity gives norm-associativity — specialized to what the conjugation needs. Only flexibility is used, which alternativity supplies.

Main results

• ConicAlgebra.isUnimodular_one : GPR 16.7.
• ConicAlgebra.norm_eq_of_projective : uniqueness of a conic norm on a finite projective algebra, GPR 16.16.
• ConicAlgebra.traceDefect_eq_zero_of_projective : GPR 16.14(b) for the trace defect.
• ConicAlgebra.conj_mul_of_projective : conjugation is an anti-homomorphism.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.15, 16.7, 16.14(b), 16.16, 17.6.

The trace defect as a linear form

theorem ConicAlgebra.traceDefect_add_left {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (x x' y : A) : C.traceDefect (x + x') y = C.traceDefect x y + C.traceDefect x' y

def ConicAlgebra.traceDefectLeft {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] (C : ConicAlgebra k A) (y : A) : A →ₗ[k] k

The trace defect as a linear form in its first argument.

Equations

• C.traceDefectLeft y = { toFun := fun (x : A) => C.traceDefect x y, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ConicAlgebra.traceDefectLeft_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [IsScalarTower k A A] (C : ConicAlgebra k A) (x y : A) : (C.traceDefectLeft y) x = C.traceDefect x y

GPR 16.7: the unit is unimodular

noncomputable def ConicAlgebra.unitForm {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) [Module.Finite k A] [Module.Projective k A] : A →ₗ[k] k

The linear form b(1, ·) for a bilinear form b representing the norm. It sends 1 to 1 (ConicAlgebra.unitForm_one), which is what makes the unit unimodular.

Equations

• C.unitForm = (QuadraticMap.bilinRepr C.norm) 1

@[simp]

theorem ConicAlgebra.unitForm_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) [Module.Finite k A] [Module.Projective k A] : C.unitForm 1 = 1

theorem ConicAlgebra.isUnimodular_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) [Module.Finite k A] [Module.Projective k A] : Module.IsUnimodular k 1

GPR 16.7. In a conic algebra that is finitely generated projective as a module, the unit is unimodular. This is GPR 11.15 for the pointed quadratic module (A, n, 1): over a projective module the norm is b(x, x) for a bilinear b, and b(1, ·) sends 1 to n 1 = 1.

theorem ConicAlgebra.norm_eq_of_projective {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [Module.Finite k A] [Module.Projective k A] (C D : ConicAlgebra k A) : C.norm = D.norm

Uniqueness of the conic norm on a finitely generated projective algebra (GPR 16.16).

Multiplicativity and non-degeneracy are not needed: projectivity makes 1 unimodular, which is the exact module-theoretic input consumed by the proof.

GPR 16.14(b): the trace defect vanishes

theorem ConicAlgebra.traceDefect_smul_sub_smul_one {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) [Module.Finite k A] [Module.Projective k A] [IsAlternative A] (x y : A) : C.traceDefect x y • (x - C.unitForm x • 1) = 0

The trace defect annihilates the "traceless part" x - λ(x) • 1 of its own argument.

Applying λ = ConicAlgebra.unitForm to d(x, y) • x = μ(x, y) • 1 (ConicAlgebra.traceDefect_smul_eq_smul_one) computes the right-hand scalar as μ(x, y) = d(x, y) λ(x), and the identity becomes this.

theorem ConicAlgebra.traceDefect_eq_zero_of_projective {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) [Module.Finite k A] [Module.Projective k A] [IsAlternative A] (x y : A) : C.traceDefect x y = 0

GPR 16.14(b), for the trace defect. In an alternative conic algebra whose module is finitely generated projective, the trace defect vanishes: t(xy) = t(x)t(y) - n(x, y).

⚠ Projectivity is essential — see Conic/TraceDefectCounterexample.lean for an associative conic algebra over ℤ/4, on a non-projective module, whose trace defect is 2.

theorem ConicAlgebra.trace_mul_of_projective {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) [Module.Finite k A] [Module.Projective k A] [IsAlternative A] (x y : A) : C.trace (x * y) = C.trace x * C.trace y - QuadraticMap.polar (⇑C.norm) x y

The trace is "multiplicative up to the norm": t(xy) = t(x)t(y) - n(x, y).

theorem ConicAlgebra.conj_mul_of_projective {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) [Module.Finite k A] [Module.Projective k A] [IsAlternative A] (x y : A) : C.conj (x * y) = C.conj y * C.conj x

Conjugation is an algebra anti-homomorphism for an alternative conic algebra that is finitely generated projective as a module (GPR 16.14(b), GPR 17.6).

theorem ConicAlgebra.conjIsInvolution_of_projective {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (C : ConicAlgebra k A) [Module.Finite k A] [Module.Projective k A] [IsAlternative A] : C.ConjIsInvolution

The conjugation of an alternative conic algebra on a finitely generated projective module is an involution (GPR 16.14(b)).