OAI/AlgebraicGeometry/Seshadri/Sheaves/PushforwardTensor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.PushforwardTensor.presheafHom line 17
2. def OAI.MaximalSeshadri.PushforwardTensor.hom line 31
3. lemma OAI.MaximalSeshadri.PushforwardTensor.hom_pure line 36
4. lemma OAI.MaximalSeshadri.PushforwardTensor.naturality line 46
5. def OAI.MaximalSeshadri.PullbackTensor.hom line 70
6. lemma OAI.MaximalSeshadri.PullbackTensor.unit_hom line 77
7. lemma OAI.MaximalSeshadri.PullbackTensor.naturality line 85