OAI/AlgebraicGeometry/RelativeTriviality/FiniteSections.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CampanaPeternellSix.RelativeCech.finiteRingPi line 15
2. lemma OAI.CampanaPeternellSix.RelativeCech.finite_free_evaluation line 18
3. lemma OAI.CampanaPeternellSix.RelativeCech.finite_sections_of_le_frame line 34
4. theorem OAI.CampanaPeternellSix.RelativeCech.finite_affine_sections line 48
5. lemma OAI.CampanaPeternellSix.RelativeCech.finite_restriction_sections line 80
6. theorem OAI.CampanaPeternellSix.RelativeCech.finite_affine_restriction line 93
7. lemma OAI.CampanaPeternellSix.RelativeCech.finite_affine_image line 133
8. lemma OAI.CampanaPeternellSix.RelativeCech.finite_affine_open line 151
9. lemma OAI.CampanaPeternellSix.RelativeCech.affine_image_restriction_spans line 162
10. theorem OAI.CampanaPeternellSix.RelativeCech.affine_restriction_spans line 202