Quadratic subalgebras generated by one element (GPR 19.8)

For an element u of a conic algebra, the submodule k · 1 + k · u is closed under multiplication because u² = t(u)u - n(u)1. This is the unital subalgebra denoted k[u] in GPR 19.8.

The discriminant t(u)² - 4n(u) controls whether (1,u) is a basis. If it is a unit, applying the polar form at 1 and at u to a relation a·1 + b·u = 0 gives a two-by-two linear system whose determinant is the negative discriminant, forcing a = b = 0.

Main definitions

• ConicAlgebra.spanOne : the linear map (a,b) ↦ a·1 + b·u.
• ConicAlgebra.adjoinElement : the unital non-associative subalgebra k[u].
• ConicAlgebra.normOnSpan : the norm on k·1 + k·u, in coefficient coordinates.
• ConicAlgebra.conicAdjoinElement : the restricted conic structure on k[u].
• ConicAlgebra.RegularRankTwoCompositionStructure : a witnessing abstract composition norm for condition GPR 19.8(i).
• ConicAlgebra.IsRegularRankTwoComposition : condition GPR 19.8(i).

Main results

• ConicAlgebra.adjoinElement_mul_comm and ConicAlgebra.adjoinElement_mul_assoc : k[u] is commutative and associative.
• ConicAlgebra.normOnSpan_isGPRRegular_iff_isUnit_discriminant : regularity of the restricted norm is equivalent to invertibility of the discriminant.
• ConicAlgebra.basis_and_regular_iff_isUnit_discriminant : GPR 19.8(ii) ⇔ (iii).
• ConicAlgebra.isRegularRankTwoComposition_iff_isUnit_discriminant : GPR 19.8(i) ⇔ (iii).
• ConicAlgebra.regularRankTwoComposition_iff_basisAndRegular : the full three-way equivalence.
• ConicAlgebra.quadraticSpan_injective_of_isUnit_discriminant : the unit-discriminant part of GPR 19.8, proving that (1,u) is linearly independent.
• ConicAlgebra.quadraticSpanEquiv : under that hypothesis, k² ≃ k[u].
• ConicAlgebra.exists_forall_mem_adjoinElement_of_isLGRing_of_rankAtStalk_eq_two : over an LG ring, a finitely generated projective conic algebra of constant rank two is k[u] for some u, with no composition hypothesis; hence it is commutative and associative (ConicAlgebra.mul_comm_of_isLGRing_of_rankAtStalk_eq_two, ConicAlgebra.mul_assoc_of_isLGRing_of_rankAtStalk_eq_two, GPR 16.4).

Implementation notes

Condition (i) is genuinely existential: its composition norm is not defined to be the ambient norm restricted to k[u]. In (i) ⇒ (ii), projectivity and rank two first make the canonical surjection k² → k[u] an equivalence; ConicAlgebra.norm_eq_of_projective then proves that the witnessing conic norm equals the restriction of the ambient norm. Building that equality into the definition of condition (i) would omit the uniqueness step in GPR's proof.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 11.24, 16.4, 16.7, 19.8.

def ConicAlgebra.spanOne (k : Type u) [CommRing k] {A : Type v} [NonAssocRing A] [Module k A] (u : A) : k × k →ₗ[k] A

The coefficient map (a,b) ↦ a·1 + b·u whose range is the quadratic subalgebra k[u].

Equations

• ConicAlgebra.spanOne k u = { toFun := fun (p : k × k) => p.1 • 1 + p.2 • u, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ConicAlgebra.spanOne_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (u : A) (p : k × k) : (spanOne k u) p = p.1 • 1 + p.2 • u

def ConicAlgebra.adjoinElement {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) (u : A) : NonAssocSubalgebra k A

The unital subalgebra k[u] = k·1 + k·u of GPR 19.8.

Closure under multiplication consumes only the degree-two identity of a conic algebra.

Equations

• C.adjoinElement u = { carrier := ↑(ConicAlgebra.spanOne k u).range, add_mem' := ⋯, zero_mem' := ⋯, mul_mem' := ⋯, smul_mem' := ⋯, one_mem := ⋯ }

def ConicAlgebra.spanOneToAdjoin {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) (u : A) : k × k →ₗ[k] ↥(C.adjoinElement u)

The coefficient map from k² onto the quadratic subalgebra k[u].

Equations

• C.spanOneToAdjoin u = LinearMap.codRestrict (C.adjoinElement u).toSubmodule (ConicAlgebra.spanOne k u) ⋯

@[simp]

theorem ConicAlgebra.coe_spanOneToAdjoin_apply {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) (u : A) (p : k × k) : ↑((C.spanOneToAdjoin u) p) = (spanOne k u) p

theorem ConicAlgebra.spanOneToAdjoin_surjective {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) (u : A) : Function.Surjective ⇑(C.spanOneToAdjoin u)

The coefficient map onto k[u] is always surjective.

theorem ConicAlgebra.finite_adjoinElement {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) (u : A) : Module.Finite k ↥(C.adjoinElement u)

The algebra k[u] is generated as a module by 1 and u, hence is finitely generated.

@[simp]

theorem ConicAlgebra.mem_adjoinElement_iff {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) (u x : A) : x ∈ C.adjoinElement u ↔ ∃ (a : k) (b : k), a • 1 + b • u = x

theorem ConicAlgebra.adjoinElement_mul_comm {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) (u : A) (x y : ↥(C.adjoinElement u)) : x * y = y * x

The algebra generated by one element of a conic algebra is commutative (GPR 19.8).

theorem ConicAlgebra.mul_self_mul_eq_mul_mul_self {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) (u : A) : u * u * u = u * (u * u)

Every element of a conic algebra generates an associative cube.

theorem ConicAlgebra.adjoinElement_mul_assoc {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) (u : A) (x y z : ↥(C.adjoinElement u)) : x * y * z = x * (y * z)

The algebra generated by one element of a conic algebra is associative (GPR 19.8).

@[instance_reducible]

def ConicAlgebra.adjoinElementCommRing {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) (u : A) : CommRing ↥(C.adjoinElement u)

The quadratic subalgebra k[u] as a commutative ring.

Equations

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

@[instance_reducible]

def ConicAlgebra.adjoinElementAlgebra {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) (u : A) : Algebra k ↥(C.adjoinElement u)

The quadratic subalgebra k[u] as an associative k-algebra.

Equations

• C.adjoinElementAlgebra u = Algebra.ofModule ⋯ ⋯

def ConicAlgebra.elementDiscriminant {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (u : A) : k

The discriminant attached to u, namely t(u)² - 4n(u) (GPR 19.8(iii)).

Equations

• C.elementDiscriminant u = C.trace u ^ 2 - 4 * C.norm u

def ConicAlgebra.normOnSpan {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (u : A) : QuadraticForm k (k × k)

The restriction of the norm to k·1 + k·u, written in coefficient coordinates.

Equations

• C.normOnSpan u = QuadraticMap.comp C.norm (ConicAlgebra.spanOne k u)

def ConicAlgebra.normAdjoinElement {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) (u : A) : QuadraticForm k ↥(C.adjoinElement u)

The norm of C restricted to the quadratic subalgebra k[u].

Equations

• C.normAdjoinElement u = C.normRestrict (C.adjoinElement u)

@[simp]

theorem ConicAlgebra.normAdjoinElement_apply {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) (u : A) (x : ↥(C.adjoinElement u)) : (C.normAdjoinElement u) x = C.norm ↑x

def ConicAlgebra.conicAdjoinElement {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) (u : A) : ConicAlgebra k ↥(C.adjoinElement u)

The conic structure on the quadratic subalgebra k[u], obtained by restricting the norm.

Equations

• C.conicAdjoinElement u = C.restrict (C.adjoinElement u)

@[simp]

theorem ConicAlgebra.normOnSpan_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (u : A) (p : k × k) : (C.normOnSpan u) p = p.1 ^ 2 + p.1 * p.2 * C.trace u + p.2 ^ 2 * C.norm u

theorem ConicAlgebra.spanOne_mul {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) (u : A) (p q : k × k) : (spanOne k u) p * (spanOne k u) q = (spanOne k u) (p.1 * q.1 - p.2 * q.2 * C.norm u, p.1 * q.2 + p.2 * q.1 + p.2 * q.2 * C.trace u)

Multiplication in the coefficient presentation of k[u].

theorem ConicAlgebra.isMultiplicative_conicAdjoinElement {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) (u : A) : (C.conicAdjoinElement u).IsMultiplicative

The restricted norm on k[u] is multiplicative (GPR 19.8(i)).

def ConicAlgebra.dualProdCoordinates {k : Type u} [CommRing k] : Module.Dual k (k × k) ≃ₗ[k] k × k

Coordinates on the dual of k × k, obtained by evaluation on (1,0) and (0,1).

Equations

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

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

The polar map of normOnSpan, with its dual output written as two coordinates.

Equations

• C.polarSpanCoordinates u = ↑ConicAlgebra.dualProdCoordinates ∘ₗ QuadraticMap.polarBilin (C.normOnSpan u)

@[simp]

theorem ConicAlgebra.polarSpanCoordinates_apply {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (u : A) (p : k × k) : (C.polarSpanCoordinates u) p = (2 * p.1 + C.trace u * p.2, C.trace u * p.1 + 2 * C.norm u * p.2)

theorem ConicAlgebra.normOnSpan_isGPRRegular_iff_bijective_polarSpanCoordinates {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (u : A) : (C.normOnSpan u).IsGPRRegular ↔ Function.Bijective ⇑(C.polarSpanCoordinates u)

The coefficient norm is regular exactly when its coordinate polar map is bijective.

theorem ConicAlgebra.bijective_polarSpanCoordinates_iff_isUnit_discriminant {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (u : A) : Function.Bijective ⇑(C.polarSpanCoordinates u) ↔ IsUnit (C.elementDiscriminant u)

The two-by-two polar matrix is bijective exactly when its discriminant is a unit.

Bijectivity of an endomorphism is invertibility (Module.End.isUnit_iff), which the matrix algebra equivalence turns into invertibility of the Gram matrix !![2, t(u); t(u), 2n(u)], hence of its determinant 4n(u) - t(u)². That is the negative of the discriminant.

theorem ConicAlgebra.normOnSpan_isGPRRegular_iff_isUnit_discriminant {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) (u : A) : (C.normOnSpan u).IsGPRRegular ↔ IsUnit (C.elementDiscriminant u)

GPR 19.8, regularity criterion. The norm on k·1 + k·u, in coefficient coordinates, is regular if and only if t(u)² - 4n(u) is a unit.

theorem ConicAlgebra.trace_eq_zero_of_smul_one_add_smul_eq_zero {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) {u : A} {a b : k} (h : a • 1 + b • u = 0) : 2 * a + C.trace u * b = 0

A relation a·1 + b·u = 0 gives the first row of the polar Gram matrix: 2a + t(u)b = 0.

theorem ConicAlgebra.polar_eq_zero_of_smul_one_add_smul_eq_zero {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) {u : A} {a b : k} (h : a • 1 + b • u = 0) : C.trace u * a + 2 * C.norm u * b = 0

The same relation gives the second row of the polar Gram matrix: t(u)a + 2n(u)b = 0.

theorem ConicAlgebra.eq_zero_of_smul_one_add_smul_eq_zero {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) {u : A} (hdisc : IsUnit (C.elementDiscriminant u)) {a b : k} (h : a • 1 + b • u = 0) : a = 0 ∧ b = 0

GPR 19.8, (iii) ⇒ linear independence. If t(u)² - 4n(u) is a unit, then a·1 + b·u = 0 forces a = b = 0.

theorem ConicAlgebra.quadraticSpan_injective_of_isUnit_discriminant {k : Type u} {A : Type v} [CommRing k] [NonAssocRing A] [Module k A] (C : ConicAlgebra k A) {u : A} (hdisc : IsUnit (C.elementDiscriminant u)) : Function.Injective ⇑(spanOne k u)

theorem ConicAlgebra.basis_and_regular_iff_isUnit_discriminant {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) (u : A) : Function.Bijective ⇑(C.spanOneToAdjoin u) ∧ (C.normOnSpan u).IsGPRRegular ↔ IsUnit (C.elementDiscriminant u)

GPR 19.8, (ii) ⇔ (iii). The pair (1,u) is a basis of k[u] and the restricted norm is regular if and only if t(u)² - 4n(u) is a unit. The restricted norm is written through this basis as normOnSpan.

noncomputable def ConicAlgebra.quadraticSpanEquiv {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) {u : A} (hdisc : IsUnit (C.elementDiscriminant u)) : (k × k) ≃ₗ[k] ↥(C.adjoinElement u)

Under the unit-discriminant hypothesis, (1,u) is a basis of k[u], expressed as a linear equivalence k × k ≃ k[u].

Equations

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

theorem ConicAlgebra.rankAtStalk_adjoinElement {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) [Nontrivial k] {u : A} (hdisc : IsUnit (C.elementDiscriminant u)) : Module.rankAtStalk ↥(C.adjoinElement u).toSubmodule = fun (x : PrimeSpectrum k) => 2

Under the unit-discriminant hypothesis k[u] has constant rank two, being the image of k² under quadraticSpanEquiv.

theorem ConicAlgebra.normOnSpan_eq_comp_quadraticSpanEquiv {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) {u : A} (hdisc : IsUnit (C.elementDiscriminant u)) : C.normOnSpan u = QuadraticMap.comp (C.normAdjoinElement u) ↑(C.quadraticSpanEquiv hdisc)

The coefficient norm is the restricted norm read through the coefficient equivalence. This is the form of that identification consumed by QuadraticForm.isGPRRegular_comp_linearEquiv_iff.

theorem ConicAlgebra.normAdjoinElement_isGPRRegular {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) {u : A} (hdisc : IsUnit (C.elementDiscriminant u)) : (C.normAdjoinElement u).IsGPRRegular

A unit discriminant makes the norm restricted to k[u] regular.

theorem ConicAlgebra.isComposition_conicAdjoinElement {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) {u : A} (hdisc : IsUnit (C.elementDiscriminant u)) : (C.conicAdjoinElement u).IsComposition

GPR 19.8, (iii) ⇒ (i). A unit discriminant makes k[u], with its restricted norm, a regular rank-two composition algebra. The rank-two basis is quadraticSpanEquiv.

structure ConicAlgebra.RegularRankTwoCompositionStructure {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) (u : A) : Type (max u v)

k[u] admits the structure of a regular rank-two composition algebra, the condition in GPR 19.8(i).

The composition norm is existential data and is not assumed to be the ambient norm restricted to k[u]. Identifying the two norms is a conclusion of GPR 19.8(i) ⇒ (ii), using uniqueness of conic norms on finitely generated projective algebras.

• conic : ConicAlgebra k ↥(C.adjoinElement u)

  A conic structure on the abstract algebra k[u]; its norm is not definitionally the restriction of the ambient norm.

• projective : Module.Projective k ↥(C.adjoinElement u)

  The quadratic subalgebra is projective.

• rank_two (m : Ideal k) [m.IsMaximal] : Module.rankAtStalk (k × k) { asIdeal := m, isPrime := ⋯ } = Module.rankAtStalk ↥(C.adjoinElement u) { asIdeal := m, isPrime := ⋯ }

  Its rank at every maximal ideal agrees with that of the free module k².

• regular : self.conic.norm.IsGPRRegular

  The composition norm is regular in GPR's sense.

• isMultiplicative : self.conic.IsMultiplicative

  The chosen norm permits composition.

def ConicAlgebra.IsRegularRankTwoComposition {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) (u : A) : Prop

The proposition that the abstract algebra k[u] admits a regular rank-two composition structure. The witnessing norm is intentionally existential.

Equations

• C.IsRegularRankTwoComposition u = Nonempty (C.RegularRankTwoCompositionStructure u)

theorem ConicAlgebra.RegularRankTwoCompositionStructure.isComposition {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) {u : A} (h : C.RegularRankTwoCompositionStructure u) : h.conic.IsComposition

A regular rank-two quadratic-subalgebra structure is an actual composition algebra in the sense of ConicAlgebra.IsComposition.

theorem ConicAlgebra.RegularRankTwoCompositionStructure.conic_norm_eq_normAdjoinElement {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) {u : A} (h : C.RegularRankTwoCompositionStructure u) : h.conic.norm = C.normAdjoinElement u

In condition GPR 19.8(i), the abstract composition norm on k[u] is forced to equal the ambient conic norm restricted to k[u]. This is the uniqueness step missing if condition (i) is defined using the restricted norm from the outset.

theorem ConicAlgebra.normOnSpan_isGPRRegular_of_normAdjoinElement_isGPRRegular {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) (u : A) (hbasis : Function.Bijective ⇑(C.spanOneToAdjoin u)) (hregular : (C.normAdjoinElement u).IsGPRRegular) : (C.normOnSpan u).IsGPRRegular

Pulling the restricted norm back through the coefficient equivalence preserves regularity.

theorem ConicAlgebra.isRegularRankTwoComposition_iff_isUnit_discriminant {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) (u : A) : C.IsRegularRankTwoComposition u ↔ IsUnit (C.elementDiscriminant u)

GPR 19.8, (i) ⇔ (iii). The generated algebra k[u] is a regular rank-two composition algebra if and only if t(u)² - 4n(u) is a unit.

theorem ConicAlgebra.regularRankTwoComposition_iff_basisAndRegular {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) (u : A) : C.IsRegularRankTwoComposition u ↔ Function.Bijective ⇑(C.spanOneToAdjoin u) ∧ (C.normOnSpan u).IsGPRRegular

GPR 19.8. The three conditions are equivalent: k[u] is a regular rank-two composition algebra; (1,u) is a basis and the restricted norm is regular; and the discriminant t(u)² - 4n(u) is a unit.

Constant rank two over an LG ring

theorem ConicAlgebra.exists_forall_mem_adjoinElement_of_isLGRing_of_rankAtStalk_eq_two {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] (hLG : IsLGRing k) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 2) : ∃ (u : A), ∀ (x : A), x ∈ C.adjoinElement u

A finitely generated projective conic algebra of constant rank two over an LG ring is generated by one element: A = k[u] (GPR 19.8).

The unit is unimodular (GPR 16.7), so a functional l with l 1 = 1 splits A ≃ k × ker l, and ker l is projective of constant rank one, hence free (GPR 11.24); its generator is u. GPR 23.4 uses this over a local ring, extending 1 to a basis of A. No composition, regularity or nontriviality hypothesis is needed.

theorem ConicAlgebra.mul_comm_of_isLGRing_of_rankAtStalk_eq_two {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] (hLG : IsLGRing k) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 2) (x y : A) : x * y = y * x

A finitely generated projective conic algebra of constant rank two over an LG ring is commutative, being k[u] (GPR 16.4).

theorem ConicAlgebra.mul_assoc_of_isLGRing_of_rankAtStalk_eq_two {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] (hLG : IsLGRing k) (hA : Module.rankAtStalk A = fun (x : PrimeSpectrum k) => 2) (x y z : A) : x * y * z = x * (y * z)

A finitely generated projective conic algebra of constant rank two over an LG ring is associative, being k[u] (GPR 16.4).