Universality properties of FieldOpAlgebra

def FieldSpecification.FieldOpAlgebra.universalLiftMap {𝓕 : FieldSpecification} {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A) (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0) : 𝓕.FieldOpAlgebra → A

For a field specification, 𝓕, given an algebra A and a function f : 𝓕.CrAnFieldOp → A such that the lift of f to FreeAlgebra.lift ℂ f : FreeAlgebra ℂ 𝓕.CrAnFieldOp → A is zero on the ideal defining 𝓕.FieldOpAlgebra, the corresponding map 𝓕.FieldOpAlgebra → A.

Equations

• FieldSpecification.FieldOpAlgebra.universalLiftMap f h1 = Quotient.lift ⇑((FreeAlgebra.lift ℂ) f) ⋯

@[simp]

theorem FieldSpecification.FieldOpAlgebra.universalLiftMap_ι {𝓕 : FieldSpecification} {a : 𝓕.FieldOpFreeAlgebra} {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A) (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0) : universalLiftMap f h1 (ι a) = ((FreeAlgebra.lift ℂ) f) a

def FieldSpecification.FieldOpAlgebra.universalLift {𝓕 : FieldSpecification} {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A) (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0) : 𝓕.FieldOpAlgebra →ₐ[ℂ] A

For a field specification, 𝓕, given an algebra A and a function f : 𝓕.CrAnFieldOp → A such that the lift of f to FreeAlgebra.lift ℂ f : FreeAlgebra ℂ 𝓕.CrAnFieldOp → A is zero on the ideal defining 𝓕.FieldOpAlgebra, the corresponding algebra map 𝓕.FieldOpAlgebra → A.

Equations

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

@[simp]

theorem FieldSpecification.FieldOpAlgebra.universalLift_ι {𝓕 : FieldSpecification} {a : 𝓕.FieldOpFreeAlgebra} {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A) (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0) : (universalLift f h1) (ι a) = ((FreeAlgebra.lift ℂ) f) a

theorem FieldSpecification.FieldOpAlgebra.universality {𝓕 : FieldSpecification} {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A) (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0) : ∃! g : 𝓕.FieldOpAlgebra →ₐ[ℂ] A, ⇑g ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f)

For a field specification, 𝓕, the algebra 𝓕.FieldOpAlgebra satisfies the following universal property. Let f : 𝓕.CrAnFieldOp → A be a function and g : 𝓕.FieldOpFreeAlgebra →ₐ[ℂ] A the universal lift of that function associated with the free algebra 𝓕.FieldOpFreeAlgebra. If g is zero on the ideal defining 𝓕.FieldOpAlgebra, then there exists algebra map g' : FieldOpAlgebra 𝓕 →ₐ[ℂ] A such that g' ∘ ι = g, and furthermore this algebra map is unique.