OAI/AlgebraicGeometry/Seshadri/Sheaves/OpenBaseChange.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MaximalSeshadri.OpenBaseChange.restrict_unit_appline 15 - lemma
OAI.MaximalSeshadri.OpenBaseChange.restrict_unit_app_isoline 20 - def
OAI.MaximalSeshadri.OpenBaseChange.rightSquareline 32 - def
OAI.MaximalSeshadri.OpenBaseChange.homline 39 - instance
OAI.MaximalSeshadri.OpenBaseChange.hom_isIsoline 50 - def
OAI.MaximalSeshadri.OpenBaseChange.isoline 65