English
The structure IsPresentationCore can be transported to a smaller universe with preserved core properties; the down operation ensures compatibility of descent and composition.
Русский
Структура IsPresentationCore может переноситься в меньшую вселенную с сохранением основных свойств; операция down обеспечивает совместимость десцентирования и композиции.
LaTeX
$$$$ \\mathrm{down}(h) : \\mathrm{IsPresentationCore}^{w''} solution \\to \\mathrm{IsPresentationCore}^{w''} solution $$$$
Lean4
/-- The structure `IsPresentationCore` can be shrunk to a lower universe. -/
def down (h : IsPresentationCore.{max w' w''} solution) : IsPresentationCore.{w''} solution
where
desc s := ULift.moduleEquiv.toLinearMap.comp (h.desc (s.postcomp ULift.moduleEquiv.symm.toLinearMap))
postcomp_desc
s := by
simpa using
congr_postcomp (h.postcomp_desc (s.postcomp ULift.moduleEquiv.symm.toLinearMap)) ULift.moduleEquiv.toLinearMap
postcomp_injective {N _ _ f f'}
h' := by
ext x
have := congr_postcomp h' ULift.moduleEquiv.{_, _, w'}.symm.toLinearMap
simp only [← postcomp_comp] at this
simpa using DFunLike.congr_fun (h.postcomp_injective this) x
