English
If g ∘ f = e and QuasispectrumRestricts a f and QuasispectrumRestricts a g hold, then QuasispectrumRestricts a e.
Русский
Если g ∘ f = e и выполнены условия ограничений через f и через g, то выполняется ограничение через e.
LaTeX
$$$g \\circ f = e \\land \\mathrm{QuasispectrumRestricts}(a,f) \\land \\mathrm{QuasispectrumRestricts}(a,g) \\Rightarrow \\mathrm{QuasispectrumRestricts}(a,e)$$$
Lean4
protected theorem comp {R₁ R₂ R₃ A : Type*} [Semifield R₁] [Field R₂] [Field R₃] [NonUnitalRing A] [Module R₁ A]
[Module R₂ A] [Module R₃ A] [Algebra R₁ R₂] [Algebra R₂ R₃] [Algebra R₁ R₃] [IsScalarTower R₁ R₂ R₃]
[IsScalarTower R₂ R₃ A] [IsScalarTower R₃ A A] [SMulCommClass R₃ A A] {a : A} {f : R₃ → R₂} {g : R₂ → R₁}
{e : R₃ → R₁} (hfge : g ∘ f = e) (hf : QuasispectrumRestricts a f) (hg : QuasispectrumRestricts a g) :
QuasispectrumRestricts a e
where
left_inv := by
convert hfge ▸ hf.left_inv.comp hg.left_inv
congrm (⇑$(IsScalarTower.algebraMap_eq R₁ R₂ R₃))
rightInvOn := by
convert hfge ▸ hg.rightInvOn.comp hf.rightInvOn fun _ ↦ hf.apply_mem
congrm (⇑$(IsScalarTower.algebraMap_eq R₁ R₂ R₃))
