Unital subalgebras of non-associative algebras

Mathlib's Subalgebra requires an associative Semiring, while its NonUnitalSubalgebra works for a NonUnitalNonAssocSemiring. Composition algebras are unital but need not be associative, so neither object alone represents their unital subalgebras. This file adds the missing one-field wrapper.

Main definitions

• NonAssocSubalgebra R A : a mathlib NonUnitalSubalgebra R A containing 1.

Implementation notes

⚠ This is deliberately not named Subalgebra: mathlib owns that name for associative algebras. The underlying multiplication and scalar-action API is inherited from NonUnitalSubalgebra; only the unit is new. With it a NonAssocSubalgebra is a SubringClass, from which mathlib supplies the unit, the casts and the NonAssocRing structure on each subalgebra (SubringClass.toNonAssocRing).

structure NonAssocSubalgebra (R : Type u) (A : Type v) [CommRing R] [NonAssocRing A] [Module R A] extends NonUnitalSubalgebra R A : Type v

A unital subalgebra of a possibly non-associative algebra.

• carrier : Set A
• add_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier
• mul_mem' {a b : A} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• smul_mem' (c : R) {x : A} : x ∈ self.carrier → c • x ∈ self.carrier
• one_mem : 1 ∈ self.carrier

  The ambient unit belongs to the subalgebra.

@[instance_reducible]

instance NonAssocSubalgebra.instSetLike {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] : SetLike (NonAssocSubalgebra R A) A

Equations

• NonAssocSubalgebra.instSetLike = { coe := fun (S : NonAssocSubalgebra R A) => S.carrier, coe_injective := ⋯ }

instance NonAssocSubalgebra.instSubringClass {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] : SubringClass (NonAssocSubalgebra R A) A

instance NonAssocSubalgebra.instSMulMemClass {R : Type u} {A : Type v} [CommRing R] [NonAssocRing A] [Module R A] : SMulMemClass (NonAssocSubalgebra R A) R A