AlgHom.exists_finitePresentation_coequalizer
Parallel maps into a finite, finitely presented stage that agree over B become equal in an actual finite, finitely presented quotient over B. The quotient remains in the original stage's universe.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
namespace AlgHomLean source · statement
theorem exists_finitePresentation_coequalizer
(R : Type u) [CommRing R] (A : Type w) [CommRing A] [Algebra R A]
[Algebra.FiniteType R A] (C : Type u) [CommRing C] [Algebra R C]
[Module.Finite R C] [Algebra.FinitePresentation R C]
(B : Type v) [CommRing B] [Algebra R B]
(f g : A →ₐ[R] C) (φ : C →ₐ[R] B) (hφ : φ.comp f = φ.comp g) :
∃ Q : CommAlgCat.{u} R, Module.Finite R Q ∧ Algebra.FinitePresentation R Q ∧
∃ (q : C →ₐ[R] Q) (ψ : Q →ₐ[R] B),
Function.Surjective q ∧ ψ.comp q = φ ∧ q.comp f = q.comp g