L-twisted 2-by-2 matrices (GPR 22.12, 22.13)

For L a k-module, the L-twisted 2-by-2 matrices are the formal matrices

[ρ₁ u*] [v ρ₂], ρᵢ ∈ k, u* ∈ L*, v ∈ L,

multiplied as matrices, using the canonical pairing L* × L → k wherever a product of an entry of L* with an entry of L occurs (GPR 22.12):

[ρ₁ u*] [σ₁ w*] [ ρ₁σ₁ + ⟨u*, z⟩ ρ₁w* + σ₂u* ] [v ρ₂] [z σ₂] = [ σ₁v + ρ₂z ρ₂σ₂ + ⟨w*, v⟩ ],

with norm ρ₁ρ₂ - ⟨u*, v⟩, trace ρ₁ + ρ₂ and conjugation exchanging the diagonal and negating the off-diagonal entries — GPR (22.12.1), (22.12.2), (22.12.3). When L is a line bundle this is GPR's presentation of Endₖ(k ⊕ L), the quaternion algebra of L-twisted matrices, and by GPR 22.13 every reduced quaternion algebra is one of these.

What is proved here

Both directions of GPR 22.13:

• the conic structure, its norm, trace and conjugation — for any k-module L;
• non-singularity of the norm for L finitely generated projective — and not by a computation: the norm is the hyperbolic form of k ⊕ L, pairing (ρ₁, u*) against (ρ₂, -v), so QuadraticForm.isGPRNonsingular_dualProd applies with no basis, no rank hypothesis and no hypothesis on 2;
• multiplicativity of the norm exactly under the identity Module.IsRankOnePairing, ⟨φ, x⟩⟨ψ, y⟩ = ⟨φ, y⟩⟨ψ, x⟩ — what the algebra needs L to have rank one for, and the only place the rank enters;
• hence that it is a composition algebra, and a reduced one: the matrix unit e₁₁ is an elementary idempotent (GPR (22.12.4)), so GPR 22.9 applies to it.
• conversely, a reduced composition algebra of constant rank four is isomorphic to the twisted matrices for its lower-left Peirce component. The Peirce rank count makes that component a line bundle, and the regular polar pairing identifies the upper-right component with its dual.

The general-purpose equivalence Module.invertible_iff_isLocallyFreeRankOne proves that a line bundle satisfies Module.IsRankOnePairing. Thus the construction gives a composition algebra for every invertible L, with no freeness assumption.

Main definitions

• Module.IsRankOnePairing k L : the identity ⟨φ, x⟩⟨ψ, y⟩ = ⟨φ, y⟩⟨ψ, x⟩.
• ConicAlgebra.TwistedMat k L : the module of L-twisted matrices, with its multiplication.
• ConicAlgebra.twistedMatNorm k L, ConicAlgebra.twistedMat k L : the norm and the conic structure.

Main results

• ConicAlgebra.isGPRNonsingular_twistedMatNorm : the norm is hyperbolic, hence non-singular.
• ConicAlgebra.isMultiplicative_twistedMat : the norm permits composition, given the rank-one pairing identity.
• ConicAlgebra.isComposition_twistedMat : it is a composition algebra.
• ConicAlgebra.isComposition_twistedMat_of_invertible : the line-bundle form of GPR 22.12.
• ConicAlgebra.hasElementaryIdempotent_twistedMat : it is reduced — GPR 22.13's easy half.
• ConicAlgebra.IsElementaryIdempotent.isomorphic_twistedMat : every reduced constant-rank-four composition algebra is a twisted-matrix algebra, the converse half of GPR 22.13.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 22.9, 22.12, 22.13.

def ConicAlgebra.TwistedMat (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : Type (max u v)

The k-module of L-twisted 2-by-2 matrices (GPR 22.12), as a type synonym for (k × L*) × (k × L): the element x is the matrix

[x.1.1 x.1.2] [x.2.2 x.2.1]

whose top row is x.1 = (ρ₁, u*) and whose bottom row is (x.2.2, x.2.1) = (v, ρ₂). The synonym is needed because the multiplication is not the componentwise one; the grouping puts the two diagonal entries first in their pairs, so that the norm is visibly the pairing of x.1 against x.2.

Equations

• ConicAlgebra.TwistedMat k L = ((k × Module.Dual k L) × k × L)

@[instance_reducible]

instance ConicAlgebra.TwistedMat.instAddCommGroup (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : AddCommGroup (TwistedMat k L)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ConicAlgebra.TwistedMat.instModule (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : Module k (TwistedMat k L)

Equations

• ConicAlgebra.TwistedMat.instModule k L = { smul := ConicAlgebra.TwistedMat.instModule._aux_1 k L, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance ConicAlgebra.TwistedMat.instFiniteOfProjective (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] [Module.Finite k L] [Module.Projective k L] : Module.Finite k (TwistedMat k L)

instance ConicAlgebra.TwistedMat.instProjectiveOfFinite (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] [Module.Finite k L] [Module.Projective k L] : Module.Projective k (TwistedMat k L)

theorem ConicAlgebra.TwistedMat.ext {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] {x y : TwistedMat k L} (h₁ : x.1.1 = y.1.1) (h₂ : x.1.2 = y.1.2) (h₃ : x.2.1 = y.2.1) (h₄ : x.2.2 = y.2.2) : x = y

Two twisted matrices agree as soon as their four entries do.

@[simp]

theorem ConicAlgebra.TwistedMat.fst_zero {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] : 0.1 = 0

@[simp]

theorem ConicAlgebra.TwistedMat.fst_neg {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x : TwistedMat k L) : (-x).1 = -x.1

@[simp]

theorem ConicAlgebra.TwistedMat.snd_neg {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x : TwistedMat k L) : (-x).2 = -x.2

@[simp]

theorem ConicAlgebra.TwistedMat.fst_sub {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : (x - y).1 = x.1 - y.1

@[simp]

theorem ConicAlgebra.TwistedMat.snd_sub {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : (x - y).2 = x.2 - y.2

@[simp]

theorem ConicAlgebra.TwistedMat.snd_zero {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] : 0.2 = 0

@[simp]

theorem ConicAlgebra.TwistedMat.fst_add {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : (x + y).1 = x.1 + y.1

@[simp]

theorem ConicAlgebra.TwistedMat.snd_add {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : (x + y).2 = x.2 + y.2

@[simp]

theorem ConicAlgebra.TwistedMat.fst_smul {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (c : k) (x : TwistedMat k L) : (c • x).1 = c • x.1

@[simp]

theorem ConicAlgebra.TwistedMat.snd_smul {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (c : k) (x : TwistedMat k L) : (c • x).2 = c • x.2

@[instance_reducible]

instance ConicAlgebra.TwistedMat.instMul (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : Mul (TwistedMat k L)

Matrix multiplication of twisted matrices, GPR 22.12: the entries of L* and of L multiply through the canonical pairing.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance ConicAlgebra.TwistedMat.instOne (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : One (TwistedMat k L)

The identity matrix.

Equations

• ConicAlgebra.TwistedMat.instOne k L = { one := ((1, 0), 1, 0) }

@[simp]

theorem ConicAlgebra.TwistedMat.mul_fst_fst {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : (x * y).1.1 = x.1.1 * y.1.1 + x.1.2 y.2.2

@[simp]

theorem ConicAlgebra.TwistedMat.mul_fst_snd {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : (x * y).1.2 = x.1.1 • y.1.2 + y.2.1 • x.1.2

@[simp]

theorem ConicAlgebra.TwistedMat.mul_snd_fst {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : (x * y).2.1 = x.2.1 * y.2.1 + y.1.2 x.2.2

@[simp]

theorem ConicAlgebra.TwistedMat.mul_snd_snd {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : (x * y).2.2 = y.1.1 • x.2.2 + x.2.1 • y.2.2

@[simp]

theorem ConicAlgebra.TwistedMat.one_fst_fst {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] : 1.1.1 = 1

@[simp]

theorem ConicAlgebra.TwistedMat.one_fst_snd {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] : 1.1.2 = 0

@[simp]

theorem ConicAlgebra.TwistedMat.one_snd_fst {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] : 1.2.1 = 1

@[simp]

theorem ConicAlgebra.TwistedMat.one_snd_snd {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] : 1.2.2 = 0

@[instance_reducible]

instance ConicAlgebra.TwistedMat.instNonAssocRing (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : NonAssocRing (TwistedMat k L)

Equations

• One or more equations did not get rendered due to their size.

instance ConicAlgebra.TwistedMat.instSMulCommClass (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : SMulCommClass k (TwistedMat k L) (TwistedMat k L)

instance ConicAlgebra.TwistedMat.instIsScalarTower (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : IsScalarTower k (TwistedMat k L) (TwistedMat k L)

The norm

n = ρ₁ρ₂ - ⟨u*, v⟩ is the pairing of the top row against the bottom row, once the bottom row is read in k ⊕ L and the top row in its dual. That is what makes it hyperbolic.

def ConicAlgebra.dualProdEquiv (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : (k × Module.Dual k L) ≃ₗ[k] Module.Dual k (k × L)

The identification k × L* ≃ (k ⊕ L)* sending (ρ, u*) to (a, w) ↦ ρa - ⟨u*, w⟩. The sign is what turns the norm below into the hyperbolic pairing.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConicAlgebra.dualProdEquiv_apply {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (p : k × Module.Dual k L) (w : k × L) : ((dualProdEquiv k L) p) w = p.1 * w.1 - p.2 w.2

def ConicAlgebra.twistedMatDualProdEquiv (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : TwistedMat k L ≃ₗ[k] Module.Dual k (k × L) × k × L

The linear equivalence presenting a twisted matrix as an element of (k ⊕ L)* ⊕ (k ⊕ L), under which the norm becomes the hyperbolic form QuadraticForm.dualProd k (k × L).

Equations

• ConicAlgebra.twistedMatDualProdEquiv k L = (ConicAlgebra.dualProdEquiv k L).prodCongr (LinearEquiv.refl k (k × L))

@[simp]

theorem ConicAlgebra.twistedMatDualProdEquiv_apply (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] (x : TwistedMat k L) : (twistedMatDualProdEquiv k L) x = ((dualProdEquiv k L) x.1, x.2)

def ConicAlgebra.twistedMatNorm (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : QuadraticForm k (TwistedMat k L)

The norm of a twisted matrix, GPR (22.12.1): n = ρ₁ρ₂ - ⟨u*, v⟩, the determinant.

Equations

• ConicAlgebra.twistedMatNorm k L = QuadraticMap.comp (QuadraticForm.dualProd k (k × L)) ↑(ConicAlgebra.twistedMatDualProdEquiv k L)

@[simp]

theorem ConicAlgebra.twistedMatNorm_apply {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x : TwistedMat k L) : (twistedMatNorm k L) x = x.1.1 * x.2.1 - x.1.2 x.2.2

theorem ConicAlgebra.polar_twistedMatNorm {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x y : TwistedMat k L) : QuadraticMap.polar (⇑(twistedMatNorm k L)) x y = x.1.1 * y.2.1 + y.1.1 * x.2.1 - x.1.2 y.2.2 - y.1.2 x.2.2

@[simp]

theorem ConicAlgebra.polar_twistedMatNorm_one {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x : TwistedMat k L) : QuadraticMap.polar (⇑(twistedMatNorm k L)) 1 x = x.1.1 + x.2.1

def ConicAlgebra.twistedMat (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : ConicAlgebra k (TwistedMat k L)

GPR 22.12: the twisted matrices form a conic algebra, with norm ρ₁ρ₂ - ⟨u*, v⟩ and trace ρ₁ + ρ₂. No hypothesis on L at all, and none on 2.

Equations

• ConicAlgebra.twistedMat k L = { norm := ConicAlgebra.twistedMatNorm k L, norm_one := ⋯, mul_self := ⋯ }

@[simp]

theorem ConicAlgebra.twistedMat_norm {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] : (twistedMat k L).norm = twistedMatNorm k L

@[simp]

theorem ConicAlgebra.trace_twistedMat_apply {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x : TwistedMat k L) : (twistedMat k L).trace x = x.1.1 + x.2.1

The trace of a twisted matrix is the sum of its diagonal entries, GPR (22.12.2).

@[simp]

theorem ConicAlgebra.conj_twistedMat_apply {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (x : TwistedMat k L) : (twistedMat k L).conj x = ((x.2.1, -x.1.2), x.1.1, -x.2.2)

The conjugation exchanges the diagonal entries and negates the off-diagonal ones, GPR (22.12.3).

Non-singularity, multiplicativity, and the composition algebra

theorem ConicAlgebra.isGPRNonsingular_twistedMatNorm (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] [Module.Finite k L] [Module.Projective k L] : (twistedMatNorm k L).IsGPRNonsingular

The norm of the twisted matrices is non-singular for L finitely generated projective: it is the hyperbolic form of k ⊕ L. No rank hypothesis and no hypothesis on 2.

theorem ConicAlgebra.isMultiplicative_twistedMat {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (h : Module.IsRankOnePairing k L) : (twistedMat k L).IsMultiplicative

The norm of the twisted matrices permits composition exactly when L has the rank-one pairing identity: expanding n(xy) and n(x)n(y) leaves precisely the difference ⟨u*, z⟩⟨w*, v⟩ - ⟨u*, v⟩⟨w*, z⟩.

theorem ConicAlgebra.isComposition_twistedMat {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] [Module.Finite k L] [Module.Projective k L] (h : Module.IsRankOnePairing k L) : (twistedMat k L).IsComposition

The twisted matrices form a composition algebra, for L finitely generated projective with the rank-one pairing identity — that is, for L a line bundle. This is the object of GPR 22.12.

theorem ConicAlgebra.isComposition_twistedMat_of_invertible {k : Type u} [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] [Module.Invertible k L] : (twistedMat k L).IsComposition

GPR 22.12. Twisted matrices attached to an invertible module form a composition algebra. The required rank-one pairing identity follows from Module.invertible_iff_isLocallyFreeRankOne.

theorem ConicAlgebra.hasElementaryIdempotent_twistedMat (k : Type u) [CommRing k] (L : Type v) [AddCommGroup L] [Module k L] : (twistedMat k L).HasElementaryIdempotent

GPR 22.13, the easy half: the algebra of L-twisted matrices is reduced. The matrix unit e₁₁ of GPR (22.12.4) has norm 0 and trace 1, so it is an elementary idempotent and GPR 22.9 applies: the norm is isotropic and the algebra contains a split quadratic étale subalgebra. No hypothesis on L.

GPR 22.13: every reduced quaternion algebra is twisted matrices

@[reducible, inline]

abbrev ConicAlgebra.IsElementaryIdempotent.TwistingModule (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] (c : A) : Submodule k A

The lower-left Peirce component used as the twisting line bundle in GPR 22.13.

Equations

• ConicAlgebra.IsElementaryIdempotent.TwistingModule k c = IsAlternative.peirceComponent c true false

noncomputable def ConicAlgebra.IsElementaryIdempotent.twistedMatToPeirce (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : TwistedMat k ↥(TwistingModule k c) →ₗ[k] A

The Peirce-coordinate map from twisted matrices to a reduced rank-four composition algebra. The upper-right coordinate uses the negative polar duality, matching the convention n([[a,φ],[v,b]]) = ab - φ(v) in GPR (22.12.1).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConicAlgebra.IsElementaryIdempotent.twistedMatToPeirce_apply (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (x : TwistedMat k ↥(TwistingModule k c)) : (twistedMatToPeirce k hc hcomp hA) x = peirceElement c x.1.1 x.2.1 ((hc.offDiagonalDuality ⋯ ⋯).symm (-x.1.2)) x.2.2

theorem ConicAlgebra.IsElementaryIdempotent.bijective_twistedMatToPeirce (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : Function.Bijective ⇑(twistedMatToPeirce k hc hcomp hA)

The Peirce-coordinate map is bijective. This is the additive decomposition and the regular off-diagonal duality assembled into one map.

noncomputable def ConicAlgebra.IsElementaryIdempotent.twistedMatEquiv (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : TwistedMat k ↥(TwistingModule k c) ≃ₗ[k] A

The linear equivalence underlying the converse half of GPR 22.13.

Equations

• ConicAlgebra.IsElementaryIdempotent.twistedMatEquiv k hc hcomp hA = LinearEquiv.ofBijective (ConicAlgebra.IsElementaryIdempotent.twistedMatToPeirce k hc hcomp hA) ⋯

@[simp]

theorem ConicAlgebra.IsElementaryIdempotent.twistedMatEquiv_apply (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (x : TwistedMat k ↥(TwistingModule k c)) : (twistedMatEquiv k hc hcomp hA) x = (twistedMatToPeirce k hc hcomp hA) x

theorem ConicAlgebra.IsElementaryIdempotent.norm_twistedMatEquiv (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (x : TwistedMat k ↥(TwistingModule k c)) : C.norm ((twistedMatEquiv k hc hcomp hA) x) = (twistedMatNorm k ↥(TwistingModule k c)) x

The equivalence of GPR 22.13 preserves the norm.

theorem ConicAlgebra.IsElementaryIdempotent.twistedMatEquiv_one (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : (twistedMatEquiv k hc hcomp hA) 1 = 1

The equivalence of GPR 22.13 is unital.

theorem ConicAlgebra.IsElementaryIdempotent.twistedMatEquiv_mul (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) (x y : TwistedMat k ↥(TwistingModule k c)) : (twistedMatEquiv k hc hcomp hA) (x * y) = (twistedMatEquiv k hc hcomp hA) x * (twistedMatEquiv k hc hcomp hA) y

The equivalence of GPR 22.13 is multiplicative.

theorem ConicAlgebra.IsElementaryIdempotent.invertible_twistingModule (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : Module.Invertible k ↥(TwistingModule k c)

The lower-left Peirce component of a reduced rank-four composition algebra is a line bundle, as required in GPR 22.13.

noncomputable def ConicAlgebra.IsElementaryIdempotent.twistedMatIsometryEquiv (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : QuadraticMap.IsometryEquiv (twistedMat k ↥(TwistingModule k c)).norm C.norm

The norm isometry underlying the converse half of GPR 22.13.

Equations

• ConicAlgebra.IsElementaryIdempotent.twistedMatIsometryEquiv k hc hcomp hA = { toLinearEquiv := ConicAlgebra.IsElementaryIdempotent.twistedMatEquiv k hc hcomp hA, map_app' := ⋯ }

theorem ConicAlgebra.IsElementaryIdempotent.isomorphic_twistedMat (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] [SMulCommClass k A A] [IsScalarTower k A A] [IsAlternative A] [Module.Finite k A] [Module.Projective k A] {C : ConicAlgebra k A} {c : A} (hc : C.IsElementaryIdempotent c) (hcomp : C.IsComposition) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 4) : (twistedMat k ↥(TwistingModule k c)).Isomorphic C

GPR 22.13, the converse half: a reduced composition algebra of constant rank four is isomorphic to the twisted matrices attached to the line bundle C₂₁.

A twisted matrix algebra on a free line is split

noncomputable def ConicAlgebra.twistedMatOfBasisEquiv (k : Type u) [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (b : Module.Basis Unit k L) : TwistedMat k L ≃ₗ[k] Matrix (Fin 2) (Fin 2) k

Coordinates from twisted matrices on a based line to ordinary two-by-two matrices.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ConicAlgebra.twistedMatOfBasisEquiv_apply (k : Type u) [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (b : Module.Basis Unit k L) (x : TwistedMat k L) : (twistedMatOfBasisEquiv k b) x = !![x.1.1, x.1.2 (b ()); (b.repr x.2.2) (), x.2.1]

theorem ConicAlgebra.det_twistedMatOfBasisEquiv (k : Type u) [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (b : Module.Basis Unit k L) (x : TwistedMat k L) : ((twistedMatOfBasisEquiv k b) x).det = (twistedMatNorm k L) x

The coordinate equivalence from twisted matrices on a based line preserves the norm.

theorem ConicAlgebra.twistedMatOfBasisEquiv_one (k : Type u) [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (b : Module.Basis Unit k L) : (twistedMatOfBasisEquiv k b) 1 = 1

The coordinate equivalence from twisted matrices on a based line preserves the identity.

theorem ConicAlgebra.twistedMatOfBasisEquiv_mul (k : Type u) [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (b : Module.Basis Unit k L) (x y : TwistedMat k L) : (twistedMatOfBasisEquiv k b) (x * y) = (twistedMatOfBasisEquiv k b) x * (twistedMatOfBasisEquiv k b) y

The coordinate equivalence from twisted matrices on a based line preserves multiplication.

theorem ConicAlgebra.isomorphic_twistedMat_ofBasis (k : Type u) [CommRing k] {L : Type v} [AddCommGroup L] [Module k L] (b : Module.Basis Unit k L) : (twistedMat k L).Isomorphic (splitQuaternion k)

The splitness assertion in GPR 22.13: twisted matrices on a free line are the split quaternion algebra.