OAI/AlgebraicGeometry/Seshadri/Geometry/GeneratedEtaleCoordinates.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MaximalSeshadri.AlgebraicJets.formallyUnramified_polynomial_of_basis line 17
2. theorem OAI.MaximalSeshadri.AlgebraicJets.formallySmooth_polynomial_of_basis line 36
3. theorem OAI.MaximalSeshadri.AlgebraicJets.formallyEtale_polynomial_of_basis line 75
4. theorem OAI.MaximalSeshadri.AlgebraicJets.presentation_coordinate_formallyEtale line 87
5. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_formallyEtale_coordinates line 102
6. theorem OAI.MaximalSeshadri.AlgebraicJets.presentation_coordinate_etale line 122
7. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_etale_coordinates line 139
8. lemma OAI.MaximalSeshadri.AlgebraicJets.differentials_span_of_generators line 162
9. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_local_differential_basis line 182
10. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_local_generator_basis line 226
11. theorem OAI.MaximalSeshadri.AlgebraicJets.coordinate_map_etale line 234
12. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_local_etale_from_spanning line 252
13. lemma OAI.MaximalSeshadri.AlgebraicJets.differentials_span_of_formallyEtale line 289