OAI/AlgebraicGeometry/Seshadri/Jets/FormalEtale.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MaximalSeshadri.AlgebraicJets.quotientBaseMap line 15
2. lemma OAI.MaximalSeshadri.AlgebraicJets.quotientBaseMap_mk line 19
3. lemma OAI.MaximalSeshadri.AlgebraicJets.quotient_factor_pow_ker_nilpotent line 23
4. theorem OAI.MaximalSeshadri.AlgebraicJets.quotientBaseMap_pow_bijective line 31
5. lemma OAI.MaximalSeshadri.AlgebraicJets.quotientBaseMap_maximal_bijective line 110
6. theorem OAI.MaximalSeshadri.AlgebraicJets.local_etale_jet_equiv line 138
7. instance OAI.MaximalSeshadri.AlgebraicJets.rationalKer_isMaximal line 158
8. def OAI.MaximalSeshadri.AlgebraicJets.rationalLocalMap line 162
9. theorem OAI.MaximalSeshadri.AlgebraicJets.etale_rational_jet_equiv line 167
10. def OAI.MaximalSeshadri.AlgebraicJets.specializeTaylor line 197
11. lemma OAI.MaximalSeshadri.AlgebraicJets.specializeTaylor_augment line 201
12. lemma OAI.MaximalSeshadri.AlgebraicJets.specializeTaylor_ker_le line 207
13. lemma OAI.MaximalSeshadri.AlgebraicJets.specializeTaylor_coordinate line 226
14. lemma OAI.MaximalSeshadri.AlgebraicJets.specializeTaylor_surjective line 241
15. theorem OAI.MaximalSeshadri.AlgebraicJets.regularTaylor_detects_ideal_power line 253
16. def OAI.MaximalSeshadri.AlgebraicJets.regularTaylorCoeffs line 309
17. lemma OAI.MaximalSeshadri.AlgebraicJets.specializedTaylor_coeff line 313
18. theorem OAI.MaximalSeshadri.AlgebraicJets.regularTaylor_vanishing_iff line 325
19. theorem OAI.MaximalSeshadri.AlgebraicJets.exists_regular_jet_coeffs line 348