Realization by a quotient of a represented boundary cover

def MagnitudeConjecture.PosetSpace.RepresentableData.isoOfQuotientCover {k T : Type u} {C : Type v} [Field k] [PartialOrder T] [CategoryTheory.Category.{u, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (D : RepresentableData k T C) {X M : C} {Y : Obj k T} (c : D.obj X ⟶ Y) (hc : BoundarySurjective c) (q : X ⟶ M) (E : (D.source ⟶ M) ≃ₗ[k] Y.carrier) (hE : ∀ (f : D.source ⟶ X), E (CategoryTheory.CategoryStruct.comp f q) = c.linear f) (hlift : ∀ (t : T) (f : D.projective t ⟶ M), ∃ (g : D.projective t ⟶ X), CategoryTheory.CategoryStruct.comp g q = f) : D.obj M ≅ Y

A represented boundary cover becomes a realization after taking a quotient with the prescribed total space, provided projective maps lift.