OAI/AlgebraicGeometry/Seshadri/Geometry/EtalePointChart.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.AlgebraicJets.etale_aeval_reindex line 17
2. lemma OAI.MaximalSeshadri.AlgebraicJets.etale_aeval_center line 27
3. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_centered_etale_coordinates line 37
4. lemma OAI.MaximalSeshadri.AlgebraicJets.exists_away_map_le line 55
5. lemma OAI.MaximalSeshadri.AlgebraicJets.exists_away_map_eq_of_le line 86
6. lemma OAI.MaximalSeshadri.AlgebraicJets.unramified_map_under_local line 101
7. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_unramified_fiber_neighborhood line 120
8. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_centered_etale_point_chart line 137