Documentation Verification Report

Universality

📁 Source: PhysLean/QFT/PerturbationTheory/WickAlgebra/Universality.lean

Statistics

Metric	Count
Definitions `universalLift`, `universalLiftMap`	2
Theorems `universalLiftMap_ι`, `universalLift_ι`, `universality`	3
Total	5

FieldSpecification.WickAlgebra

Definitions

Name	Category	Theorems
`universalLift` 📖	CompOp	1 math math: `universalLift_ι`
`universalLiftMap` 📖	CompOp	1 math math: `universalLiftMap_ι`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`universalLiftMap_ι` 📖	mathematical	`FieldSpecification.CrAnFieldOp`	`universalLiftMap` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.WickAlgebra` `FieldSpecification.fieldOpIdealSet` `ι`	—	—
`universalLift_ι` 📖	mathematical	`FieldSpecification.CrAnFieldOp`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.fieldOpIdealSet` `universalLift` `ι`	—	—
`universality` 📖	mathematical	`FieldSpecification.CrAnFieldOp`	`FieldSpecification.WickAlgebra` `FieldSpecification.FieldOpFreeAlgebra` `FieldSpecification.fieldOpIdealSet` `ι`	—	`universalLift_ι` `ι_surjective`

---

← Back to Index