Physlib.QFT.PerturbationTheory.WickAlgebra.Universality

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QFT.PerturbationTheory.WickAlgebra.Basic

Universality properties of WickAlgebra

@[expose] public section

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 𝓕.WickAlgebra, the corresponding map 𝓕.WickAlgebra → A.


def universalLiftMap {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
    WickAlgebra 𝓕 → A :=
  Quotient.lift (FreeAlgebra.lift ℂ f) (by𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ∀ (a b : 𝓕.FieldOpFreeAlgebra), a ≈ b → ((FreeAlgebra.lift ℂ) f) a = ((FreeAlgebra.lift ℂ) f) b
    intro a b h𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0a:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:a ≈ b⊢ ((FreeAlgebra.lift ℂ) f) a = ((FreeAlgebra.lift ℂ) f) b
    rw [equiv_iff_exists_add𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0a:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:∃ a_1, a = b + a_1 ∧ a_1 ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ((FreeAlgebra.lift ℂ) f) a = ((FreeAlgebra.lift ℂ) f) b𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0a:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:∃ a_1, a = b + a_1 ∧ a_1 ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ((FreeAlgebra.lift ℂ) f) a = ((FreeAlgebra.lift ℂ) f) b] at h𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0a:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrah:∃ a_1, a = b + a_1 ∧ a_1 ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ((FreeAlgebra.lift ℂ) f) a = ((FreeAlgebra.lift ℂ) f) b
    obtain ⟨a, rfl, ha⟩ := h𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0b:𝓕.FieldOpFreeAlgebraa:𝓕.FieldOpFreeAlgebraha:a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ((FreeAlgebra.lift ℂ) f) (b + a) = ((FreeAlgebra.lift ℂ) f) b
    simp only [map_add]𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0b:𝓕.FieldOpFreeAlgebraa:𝓕.FieldOpFreeAlgebraha:a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ((FreeAlgebra.lift ℂ) f) b + ((FreeAlgebra.lift ℂ) f) a = ((FreeAlgebra.lift ℂ) f) b
    rw [h1 a ha𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0b:𝓕.FieldOpFreeAlgebraa:𝓕.FieldOpFreeAlgebraha:a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ((FreeAlgebra.lift ℂ) f) b + 0 = ((FreeAlgebra.lift ℂ) f) b𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0b:𝓕.FieldOpFreeAlgebraa:𝓕.FieldOpFreeAlgebraha:a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ((FreeAlgebra.lift ℂ) f) b + 0 = ((FreeAlgebra.lift ℂ) f) b]𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0b:𝓕.FieldOpFreeAlgebraa:𝓕.FieldOpFreeAlgebraha:a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet⊢ ((FreeAlgebra.lift ℂ) f) b + 0 = ((FreeAlgebra.lift ℂ) f) b
    simpAll goals completed! 🐙)

@[simp]
lemma universalLiftMap_ι {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 := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ universalLiftMap f h1 (ι a) = ((FreeAlgebra.lift ℂ) f) a rflAll goals completed! 🐙


def universalLift {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
    WickAlgebra 𝓕 →ₐ[ℂ] A where
  toFun := universalLiftMap f h1
  map_one' := by𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ universalLiftMap f h1 1 = 1
    rw [show 1 = ι (𝓕 := 𝓕) 1 from rfl,𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ universalLiftMap f h1 (ι 1) = 1𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ((FreeAlgebra.lift ℂ) f) 1 = 1 universalLiftMap_ι𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ((FreeAlgebra.lift ℂ) f) 1 = 1𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ((FreeAlgebra.lift ℂ) f) 1 = 1]𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ((FreeAlgebra.lift ℂ) f) 1 = 1
    simpAll goals completed! 🐙
  map_mul' x y := by𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0x:𝓕.WickAlgebray:𝓕.WickAlgebra⊢ universalLiftMap f h1 (x * y) = universalLiftMap f h1 x * universalLiftMap f h1 y
    obtain ⟨x, rfl⟩ := ι_surjective x𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0y:𝓕.WickAlgebrax:𝓕.FieldOpFreeAlgebra⊢ universalLiftMap f h1 (ι x * y) = universalLiftMap f h1 (ι x) * universalLiftMap f h1 y
    obtain ⟨y, rfl⟩ := ι_surjective y𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ universalLiftMap f h1 (ι x * ι y) = universalLiftMap f h1 (ι x) * universalLiftMap f h1 (ι y)
    simp [← map_mul]All goals completed! 🐙
  map_zero' := by𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ universalLiftMap f h1 0 = 0
    rw [show 0 = ι (𝓕 := 𝓕) 0 from rfl,𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ universalLiftMap f h1 (ι 0) = 0𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ((FreeAlgebra.lift ℂ) f) 0 = 0 universalLiftMap_ι𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ((FreeAlgebra.lift ℂ) f) 0 = 0𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ((FreeAlgebra.lift ℂ) f) 0 = 0]𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ((FreeAlgebra.lift ℂ) f) 0 = 0
    simpAll goals completed! 🐙
  map_add' x y := by𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0x:𝓕.WickAlgebray:𝓕.WickAlgebra⊢ universalLiftMap f h1 (x + y) = universalLiftMap f h1 x + universalLiftMap f h1 y
    obtain ⟨x, rfl⟩ := ι_surjective x𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0y:𝓕.WickAlgebrax:𝓕.FieldOpFreeAlgebra⊢ universalLiftMap f h1 (ι x + y) = universalLiftMap f h1 (ι x) + universalLiftMap f h1 y
    obtain ⟨y, rfl⟩ := ι_surjective y𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0x:𝓕.FieldOpFreeAlgebray:𝓕.FieldOpFreeAlgebra⊢ universalLiftMap f h1 (ι x + ι y) = universalLiftMap f h1 (ι x) + universalLiftMap f h1 (ι y)
    simp [← map_add]All goals completed! 🐙
  commutes' r := by𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ universalLiftMap f h1 ((algebraMap ℂ 𝓕.WickAlgebra) r) = (algebraMap ℂ A) r
    rw [Algebra.algebraMap_eq_smul_one r𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ universalLiftMap f h1 (r • 1) = (algebraMap ℂ A) r𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ universalLiftMap f h1 (r • 1) = (algebraMap ℂ A) r]𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ universalLiftMap f h1 (r • 1) = (algebraMap ℂ A) r
    rw [show r • 1 = ι (𝓕 := 𝓕) (r • 1) from rfl,𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ universalLiftMap f h1 (ι (r • 1)) = (algebraMap ℂ A) r𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ ((FreeAlgebra.lift ℂ) f) (r • 1) = (algebraMap ℂ A) r universalLiftMap_ι𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ ((FreeAlgebra.lift ℂ) f) (r • 1) = (algebraMap ℂ A) r𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ ((FreeAlgebra.lift ℂ) f) (r • 1) = (algebraMap ℂ A) r]𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ ((FreeAlgebra.lift ℂ) f) (r • 1) = (algebraMap ℂ A) r
    simp only [map_smul, map_one]𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0r:ℂ⊢ r • 1 = (algebraMap ℂ A) r
    exact Eq.symm (Algebra.algebraMap_eq_smul_one r)All goals completed! 🐙

@[simp]
lemma universalLift_ι {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 := by𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebraA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ (universalLift f h1) (ι a) = ((FreeAlgebra.lift ℂ) f) a rflAll goals completed! 🐙

For a field specification, 𝓕, the algebra 𝓕.WickAlgebra 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 𝓕.WickAlgebra, then there exists algebra map g' : WickAlgebra 𝓕 →ₐ[ℂ] A such that g' ∘ ι = g, and furthermore this algebra map is unique.

lemma universality {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
    ∃! g : WickAlgebra 𝓕 →ₐ[ℂ] A, g ∘ ι = FreeAlgebra.lift ℂ f := by𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ∃! g, ⇑g ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f)
  use universalLift f h1h𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ (fun g => ⇑g ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f)) (universalLift f h1) ∧
  ∀ (y : 𝓕.WickAlgebra →ₐ[ℂ] A), (fun g => ⇑g ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f)) y → y = universalLift f h1
  simp onlyh𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ⇑(universalLift f h1) ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f) ∧
  ∀ (y : 𝓕.WickAlgebra →ₐ[ℂ] A), ⇑y ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f) → y = universalLift f h1
  apply And.introh.left𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ⇑(universalLift f h1) ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f)h.right𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ∀ (y : 𝓕.WickAlgebra →ₐ[ℂ] A), ⇑y ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f) → y = universalLift f h1
  ·h.left𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ⇑(universalLift f h1) ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f) ext ah.left𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0a:𝓕.FieldOpFreeAlgebra⊢ (⇑(universalLift f h1) ∘ ⇑ι) a = ((FreeAlgebra.lift ℂ) f) a
    simpAll goals completed! 🐙
  ·h.right𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0⊢ ∀ (y : 𝓕.WickAlgebra →ₐ[ℂ] A), ⇑y ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f) → y = universalLift f h1 intro g hgh.right𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0g:𝓕.WickAlgebra →ₐ[ℂ] Ahg:⇑g ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f)⊢ g = universalLift f h1
    ext ah.right𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0g:𝓕.WickAlgebra →ₐ[ℂ] Ahg:⇑g ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f)a:𝓕.WickAlgebra⊢ g a = (universalLift f h1) a
    obtain ⟨a, rfl⟩ := ι_surjective ah.right𝓕:FieldSpecificationA:Typeinst✝¹:Semiring Ainst✝:Algebra ℂ Af:𝓕.CrAnFieldOp → Ah1:∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, ((FreeAlgebra.lift ℂ) f) a = 0g:𝓕.WickAlgebra →ₐ[ℂ] Ahg:⇑g ∘ ⇑ι = ⇑((FreeAlgebra.lift ℂ) f)a:𝓕.FieldOpFreeAlgebra⊢ g (ι a) = (universalLift f h1) (ι a)
    simpa using congrFun hg aAll goals completed! 🐙