[mcdoll]

This PR defines the resolvent of an unbounded operator as a linear map. There are slight differences to the way the resolvent is defined in the literature: we use a purely algebraic description, in particular we do not assume that the operator is closed.

We prove the well-known first and second resolvent identities.

---

• depends on: [Merged by Bors] - feat(LinearAlgebra): kernel of a LinearPMap #42423
• depends on: [Merged by Bors] - chore(LinearAlgebra/LinearPMap): change lemma to use LinearMap.range #42425
• depends on: [Merged by Bors] - chore: add prodComm_trans_prodComm for various cases #43923

[github-actions]

PR summary 60c1576be4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.LinearAlgebra.LinearPMap	996	1000	+4 (+0.40%)

Import changes for all files

Files	Import difference
5 files Mathlib.Analysis.Convex.StdSimplex Mathlib.Analysis.Convex.Topology Mathlib.Analysis.Convex.Visible Mathlib.Topology.Algebra.AsymptoticCone Mathlib.Topology.Algebra.Module.LocallyConvex	1
90 files Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.Algebra.Azumaya.Basic Mathlib.Algebra.Category.FGModuleCat.Abelian Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.Algebra.Category.FGModuleCat.Colimits Mathlib.Algebra.Category.FGModuleCat.EssentiallySmall Mathlib.Algebra.Category.FGModuleCat.Limits Mathlib.Algebra.Category.Grp.Injective Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Algebra.Category.ModuleCat.Ulift Mathlib.Algebra.Central.TensorProduct Mathlib.Algebra.Exact.Sequence Mathlib.Algebra.Group.UniqueProds.VectorSpace Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.Algebra.Lie.InvariantForm Mathlib.Algebra.Lie.Loop Mathlib.Algebra.Lie.Nilpotent Mathlib.Algebra.Module.Lattice Mathlib.Algebra.Module.LinearMap.Index Mathlib.Algebra.Module.Submodule.Union Mathlib.Algebra.Order.Module.HahnEmbedding Mathlib.Algebra.Star.LinearMap Mathlib.Analysis.Convex.BetweenList Mathlib.Analysis.Convex.Between Mathlib.Analysis.Convex.Caratheodory Mathlib.Analysis.Convex.Combination Mathlib.Analysis.Convex.Cone.Extension Mathlib.Analysis.Convex.Independent Mathlib.Analysis.Convex.Jensen Mathlib.Analysis.Convex.Radon Mathlib.Analysis.Convex.SimplicialComplex.AffineIndependentUnion Mathlib.Analysis.Convex.SimplicialComplex.Basic Mathlib.Analysis.Convex.StoneSeparation Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu Mathlib.FieldTheory.Finiteness Mathlib.Geometry.Convex.Cone.TensorProduct Mathlib.Geometry.Polygon.Basic Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift Mathlib.LinearAlgebra.AffineSpace.Basis Mathlib.LinearAlgebra.AffineSpace.Ceva Mathlib.LinearAlgebra.AffineSpace.Dimension Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.LinearAlgebra.AffineSpace.Independent Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid Mathlib.LinearAlgebra.Basis.MulOpposite Mathlib.LinearAlgebra.Basis.VectorSpace Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.LinearAlgebra.Coevaluation Mathlib.LinearAlgebra.Contraction Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.Dimension.ErdosKaplansky Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.LinearAlgebra.Dimension.Localization Mathlib.LinearAlgebra.Dual.Lemmas Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.LinearAlgebra.FiniteDimensional.Basic Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.LinearAlgebra.FiniteDimensional.Lemmas Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv Mathlib.LinearAlgebra.LinearIndependent.BaseChange Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.LinearAlgebra.Matrix.WithConv Mathlib.LinearAlgebra.PerfectPairing.Basic Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.LinearAlgebra.Projectivization.Collinear Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.RepresentationTheory.Basic Mathlib.RepresentationTheory.Equiv Mathlib.RepresentationTheory.Intertwining Mathlib.RepresentationTheory.Stabilizer Mathlib.RepresentationTheory.Submodule Mathlib.RepresentationTheory.Subrepresentation Mathlib.RingTheory.Bialgebra.GroupLike Mathlib.RingTheory.Bialgebra.MonoidAlgebra Mathlib.RingTheory.Coalgebra.GroupLike Mathlib.RingTheory.Flat.Domain Mathlib.RingTheory.HopfAlgebra.GroupLike Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra Mathlib.RingTheory.Length Mathlib.RingTheory.SimpleModule.InjectiveProjective Mathlib.RingTheory.SimpleModule.Rank Mathlib.RingTheory.SimpleRing.DivisionRing Mathlib.RingTheory.TensorProduct.Nontrivial	3
3 files Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Module.Injective Mathlib.LinearAlgebra.LinearPMap	4
Mathlib.LinearAlgebra.Resolvent (new file)	1293

---

Declarations diff (regex)

+ _root_.LinearMap.resolventLM_toPMap_eq_resolvent
+ _root_.LinearMap.resolventSet_toPMap
+ apply_inverseLM_apply_cancel
+ compLinearMap
+ compLinearMap_apply
+ domain_inverse_eq_top_of_surjective
+ graph_eq_map_graph_inverse
+ inverseLM
+ inverseLM_apply_apply_cancel
+ inverseLM_apply_eq
+ inverseLM_apply_eq_inverse_apply
+ inverseLM_apply_mem_domain
+ inverseLM_sub_inverseLM_eq
+ mem_inverse_domain_of_surjective
+ mem_resolventSet_iff
+ prodMk_inverseLM_mem_graph
+ prodMk_inverse_mem_graph
+ prodMk_mem_inverse_graph
+ range_inverseLM
+ range_resolventLM
+ resolventLM
+ resolventLM_apply_apply
+ resolventLM_apply_eq
+ resolventLM_comm
+ resolventLM_of_notMem_resolventSet
+ resolventLM_sub_resolventLM
+ resolventLM_sub_resolventLM'
+ resolventSet
+ resolvent_eq_iff_mul_left_eq_one
+ resolvent_eq_iff_mul_right_eq_one
+ toLinearMap
+ toLinearMap_apply_eq

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 60c1576).

• +34 new declarations
• −0 removed declarations

+LinearMap.resolventLM_toPMap_eq_resolvent
+LinearMap.resolventSet_toPMap
+LinearPMap.apply_inverseLM_apply_cancel
+LinearPMap.compLinearMap
+LinearPMap.compLinearMap_apply
+LinearPMap.domain_inverse_eq_top_of_surjective
+LinearPMap.graph_eq_map_graph_inverse
+LinearPMap.inverseLM
+LinearPMap.inverseLM.congr_simp
+LinearPMap.inverseLM_apply_apply_cancel
+LinearPMap.inverseLM_apply_eq
+LinearPMap.inverseLM_apply_eq_inverse_apply
+LinearPMap.inverseLM_apply_mem_domain
+LinearPMap.inverseLM_sub_inverseLM_eq
+LinearPMap.mem_inverse_domain_of_surjective
+LinearPMap.mem_resolventSet_iff
+LinearPMap.prodMk_inverseLM_mem_graph
+LinearPMap.prodMk_inverse_mem_graph
+LinearPMap.prodMk_mem_inverse_graph
+LinearPMap.range_inverseLM
+LinearPMap.range_resolventLM
+LinearPMap.resolventLM
+LinearPMap.resolventLM_apply_apply
+LinearPMap.resolventLM_apply_eq
+LinearPMap.resolventLM_comm
+LinearPMap.resolventLM_of_notMem_resolventSet
+LinearPMap.resolventLM_sub_resolventLM
+LinearPMap.resolventLM_sub_resolventLM'
+LinearPMap.resolventSet
+LinearPMap.toLinearMap
+LinearPMap.toLinearMap.congr_simp
+LinearPMap.toLinearMap_apply_eq
+spectrum.resolvent_eq_iff_mul_left_eq_one
+spectrum.resolvent_eq_iff_mul_right_eq_one

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
5075	1	exposed public sections

Current commit 60c1576be4
Reference commit 380f2aafb6

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mcdoll]

I am not sure of the name of inverse_asLinearMap, it is annoyingly long, is inverse_asLM or inverseLM better?

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[mathlib-merge-conflicts]

This pull request has conflicts, please merge master and resolve them.

[mcdoll]

Thanks for pointing out the other resolvent: the connection is important to prove so that the conventions agree

[YaelDillies]

Thanks!

maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[riccardobrasca]

@j-loreaux or @ADedecker can you have a final look? Thanks!

[j-loreaux]

overall this seems reasonable to me. Just a few issues.

[j-loreaux]

Some missing API I think:

Suggested change

	theorem range_resolventLM (hz : z ∈ f.resolventSet) :
	(f.resolventLM z).range = f.domain := by
	simp [resolventLM, hz, range_inverseLM hz]
	theorem range_resolventLM (hz : z ∈ f.resolventSet) :
	(f.resolventLM z).range = f.domain := by
	simp [resolventLM, hz, range_inverseLM hz]
	theorem resolventLM_apply_mem_domain (hz : z ∈ f.resolventSet) (y : E) :
	f.resolventLM z y ∈ f.domain :=
	range_resolventLM hz ▸ LinearMap.mem_range_self _ y
	theorem smul_resolventLM_apply_sub_apply (hz : z ∈ f.resolventSet) (y : E) :
	z • f.resolventLM z y - f ⟨f.resolventLM z y, resolventLM_apply_mem_domain hz y⟩ = y := by
	simpa [resolventLM, hz, vadd_apply, sub_eq_add_neg] using inverseLM_apply_apply_cancel hz y

[j-loreaux]

I realize this is longer, but it does allow to remove the extra type class assumptions. Perhaps there is an easier way?

Suggested change

	grind [smul_cancel_of_non_zero_divisor, smul_eq_zero_iff_right]
	theorem resolventLM_comm (z₁ z₂ : R) :
	f.resolventLM z₁ ∘ₗ f.resolventLM z₂ = f.resolventLM z₂ ∘ₗ f.resolventLM z₁ := by
	obtain hz | ⟨hz₁, hz₂⟩ := em (z₁ ∈ f.resolventSet ∧ z₂ ∈ f.resolventSet) |>.symm
	· grind [LinearMap.zero_comp, LinearMap.comp_zero]
	ext y
	let u : f.domain := ⟨f.resolventLM z₂ y, resolventLM_apply_mem_domain hz₂ y⟩
	let x : f.domain := ⟨f.resolventLM z₁ u, resolventLM_apply_mem_domain hz₁ u⟩
	have hu : z₂ • (u : E) - f u = y := smul_resolventLM_apply_sub_apply hz₂ y
	have hx : z₁ • (x : E) - f x = u := smul_resolventLM_apply_sub_apply hz₁ u
	have key : f.resolventLM z₁ y = ((z₂ - z₁) • x + u : f.domain) := by
	apply resolventLM_apply_eq hz₁ (Submodule.coe_mem _)
	simp only [Subtype.coe_eta, f.map_add, f.map_smul]
	rw [← hu, Submodule.coe_add, Submodule.coe_smul, ← hx]
	module
	change (x : E) = f.resolventLM z₂ (f.resolventLM z₁ y)
	rw [key, eq_comm]
	apply resolventLM_apply_eq hz₂ x.2
	rw [Submodule.coe_add, Submodule.coe_smul, ← hx]
	module

[j-loreaux]

Can you explain why this is necessary / why we should want it? I'm not totally up to speed on the transparency issues for transitions between morphism types.

[j-loreaux]

Wait, isn't it this?

Suggested change

	the case, then the conventional definition yields that `f.resolventSet = univ`
	the case, then the conventional definition yields that `f.resolventSet = ∅`

[j-loreaux]

bors d+

[mathlib-bors]

✌️ mcdoll can now approve this pull request until 2026-10-27 22:23 UTC (in 2 weeks). To approve and merge, reply with bors r+. More detailed instructions are available here.

⚠️ This delegation only covers changes within Archive/**, Counterexamples/**, docs/**, DownstreamTest/**, Mathlib/**, MathlibTest/**, Wanted/**, widget/**, Archive.lean, Counterexamples.lean, docs.lean, Mathlib.lean, Wanted.lean; an author commit touching anything else will revoke it. Bors also revokes it if a later push changes too many files for it to check the full list — even if it stays within scope.

[mathlib-bors]

⏳ @mcdoll, your delegation on this PR expires in less than a week (approximately 6 days, 23 hours, at 2026-10-27 22:23 UTC).