feat: Universality properties

HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean

@@ -41,13 +41,7 @@ def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
 - `[ofCrAnOpF φa, ofCrAnOpF φa']ₛca` for `φa` and `φa'` annihilation operators. I.e two
   annihilation operators always super-commute.
 - `[ofCrAnOpF φ, ofCrAnOpF φ']ₛca` for `φ` and `φ'` field operators with different statistics.
-  I.e. Fermions super-commute with bosons.
-
-The algebra `𝓕.FieldOpAlgebra` satisfies the following universal property. For any
-algebra `A` (e.g. the operator algebra of the theory) with a map `f : 𝓕.CrAnFieldOp → A` (e.g.
-the inclusion of the creation and annihilation parts of field operators into the operator algebra)
-such that the image of `f` obey the relations above, there exists a unique algebra map
-`g : 𝓕.FieldOpAlgebra → A` through which `f` factors. -/
+  I.e. Fermions super-commute with bosons. -/
 abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotient
 
 namespace FieldOpAlgebra
@@ -61,6 +55,18 @@ lemma equiv_iff_sub_mem_ideal (x y : FieldOpFreeAlgebra 𝓕) :
   rw [← TwoSidedIdeal.rel_iff]
   rfl
 
+lemma equiv_iff_exists_add (x y : FieldOpFreeAlgebra 𝓕) :
+    x ≈ y ↔ ∃ a, x = y + a ∧ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet := by
+  apply Iff.intro
+  · intro h
+    rw [equiv_iff_sub_mem_ideal] at h
+    use x - y
+    simp [h]
+  · intro h
+    obtain ⟨a, rfl, ha⟩ := h
+    rw [equiv_iff_sub_mem_ideal]
+    simp [ha]
+
 /-- The projection of `FieldOpFreeAlgebra` down to `FieldOpAlgebra` as an algebra map. -/
 def ι : FieldOpFreeAlgebra 𝓕 →ₐ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.mk'

HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean

@@ -0,0 +1,99 @@
+/-
+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
+-/
+import HepLean.PerturbationTheory.FieldOpAlgebra.Basic
+/-!
+
+# Universality properties of FieldOpAlgebra
+
+-/
+
+namespace FieldSpecification
+open FieldOpFreeAlgebra
+open HepLean.List
+open FieldStatistic
+
+namespace FieldOpAlgebra
+variable {𝓕 : FieldSpecification}
+
+/-- 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`.
+-/
+def universalLiftMap {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
+    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0):
+    FieldOpAlgebra 𝓕 → A :=
+  Quotient.lift (FreeAlgebra.lift ℂ f) (by
+    intro a b h
+    rw [equiv_iff_exists_add] at h
+    obtain ⟨a, rfl, ha⟩ := h
+    simp
+    rw [h1 a ha]
+    simp)
+
+@[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 rfl
+
+
+/-- 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`.
+-/
+def universalLift {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
+    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
+    FieldOpAlgebra 𝓕 →ₐ[ℂ] A where
+  toFun := universalLiftMap f h1
+  map_one' := by
+    rw [show 1 = ι (𝓕 := 𝓕) 1 from rfl, universalLiftMap_ι]
+    simp
+  map_mul' x y := by
+    obtain ⟨x, rfl⟩ := ι_surjective x
+    obtain ⟨y, rfl⟩ := ι_surjective y
+    simp [← map_mul]
+  map_zero' := by
+    simp only
+    rw [show 0 = ι (𝓕 := 𝓕) 0 from rfl, universalLiftMap_ι]
+    simp
+  map_add' x y := by
+    obtain ⟨x, rfl⟩ := ι_surjective x
+    obtain ⟨y, rfl⟩ := ι_surjective y
+    simp [← map_add]
+  commutes' r := by
+    simp only
+    rw [Algebra.algebraMap_eq_smul_one r]
+    rw [show r • 1 = ι (𝓕 := 𝓕) (r • 1) from rfl, universalLiftMap_ι]
+    simp only [map_smul, map_one]
+    exact Eq.symm (Algebra.algebraMap_eq_smul_one r)
+
+@[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 rfl
+
+/--
+For a field specification, `𝓕`, the algebra `𝓕.FieldOpAlgebra` satifies 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 is a unique
+algebra map `g' : FieldOpAlgebra 𝓕 →ₐ[ℂ] A` such that `g' ∘ ι = g`.
+-/
+lemma universality {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 := by
+  use universalLift f h1
+  simp only
+  apply And.intro
+  · ext a
+    simp
+  · intro g hg
+    ext a
+    obtain ⟨a, rfl⟩ := ι_surjective a
+    simpa using congrFun hg a
+
+end FieldOpAlgebra
+end FieldSpecification

HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean

@@ -35,17 +35,12 @@ namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
 /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is
-  the free algebra generated by `𝓕.CrAnFieldOp`.
-
-  The algebra `𝓕.FieldOpFreeAlgebra` satisfies the universal property that for any other algebra
-  `A` (e.g. the operator algebra of the theory) with a map `f : 𝓕.CrAnFieldOp → A` (e.g.
-  the inclusion of the creation and annihilation parts of field operators into the
-  operator algebra) there is a unqiue algebra map `g : 𝓕.FieldOpFreeAlgebra → A`
-  through which `f` factors. -/
+  the free algebra generated by `𝓕.CrAnFieldOp`. -/
 abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ 𝓕.CrAnFieldOp
 
 namespace FieldOpFreeAlgebra
 
+
 remark naming_convention := "
   For mathematicial objects defined in relation to `FieldOpFreeAlgebra` we will often postfix
   their names with an `F` to indicate that they are related to the free algebra.
@@ -57,6 +52,25 @@ remark naming_convention := "
 def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 :=
   FreeAlgebra.ι ℂ φ
 
+/--
+The algebra `𝓕.FieldOpFreeAlgebra` satisfies the universal property that for any other algebra
+  `A` (e.g. the operator algebra of the theory) with a map `f : 𝓕.CrAnFieldOp → A` (e.g.
+  the inclusion of the creation and annihilation parts of field operators into the
+  operator algebra) there is a unqiue algebra map `g : 𝓕.FieldOpFreeAlgebra → A`
+  such that `g ∘ ofCrAnOpF = f`.
+
+  The unique `g` is given by `FreeAlgebra.lift ℂ f`.
+-/
+lemma universality {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A) :
+    ∃! g : FieldOpFreeAlgebra 𝓕 →ₐ[ℂ] A,  g ∘ ofCrAnOpF = f := by
+  use FreeAlgebra.lift ℂ f
+  apply And.intro
+  · funext x
+    simp [ofCrAnOpF]
+  · intro g hg
+    ext x
+    simpa using congrFun hg x
+
 /-- For a field specification `𝓕`, `ofCrAnListF φs` of `𝓕.FieldOpFreeAlgebra` formed by a
   list `φs` of `𝓕.CrAnFieldOp`. For example for the list `[φ₁ᶜ, φ₂ᵃ, φ₃ᶜ]` we schematically
   get `φ₁ᶜφ₂ᵃφ₃ᶜ`. The set of all `ofCrAnListF φs` forms a basis of `FieldOpFreeAlgebra 𝓕`. -/