OAI/AlgebraicGeometry/Seshadri/Bertini/Descent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.BertiniIntegral.doubleBaseChange line 12
2. lemma OAI.MaximalSeshadri.BertiniIntegral.doubleBaseChange_tmul line 18
3. lemma OAI.MaximalSeshadri.BertiniIntegral.faithfullyFlat_dvd_iff line 24
4. theorem OAI.MaximalSeshadri.BertiniIntegral.scalar_regular_pair_descent line 32
5. lemma OAI.MaximalSeshadri.BertiniIntegral.scalar_model_injective line 48
6. theorem OAI.MaximalSeshadri.BertiniIntegral.model_line_conditions line 53
7. theorem OAI.MaximalSeshadri.BertiniIntegral.domain_hyperplane_equation_transport line 115
8. theorem OAI.MaximalSeshadri.BertiniIntegral.integral_hyperplane_section_over_model line 139
9. theorem OAI.MaximalSeshadri.BertiniIntegral.integral_hyperplane_section line 171
10. theorem OAI.MaximalSeshadri.BertiniIntegral.etale_integral_hyperplane_section line 207
11. theorem OAI.MaximalSeshadri.BertiniIntegral.hyperplane_integral_fiber_of_injective line 267
12. theorem OAI.MaximalSeshadri.BertiniIntegral.hyperplane_integral_equation_of_injective line 298