OAI/AlgebraicGeometry/Seshadri/Jets/CoordinateEquivalences.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MaximalSeshadri.FormalCoordinates.ringEnd_injective_of_surjective line 13
2. lemma OAI.MaximalSeshadri.FormalCoordinates.complete_maximal line 44
3. lemma OAI.MaximalSeshadri.FormalCoordinates.map_maximal_eq_of_cotangent line 48
4. lemma OAI.MaximalSeshadri.FormalCoordinates.bijective_of_cotangent line 59
5. def OAI.MaximalSeshadri.FormalCoordinates.equivOfCotangent line 79
6. lemma OAI.MaximalSeshadri.FormalCoordinates.equiv_comap_pow_maximal line 86
7. lemma OAI.MaximalSeshadri.FormalCoordinates.mem_maximal_pow_iff line 98
8. lemma OAI.MaximalSeshadri.FormalCoordinates.mem_maximal_sq_iff line 107
9. lemma OAI.MaximalSeshadri.FormalCoordinates.subst_bijective_of_inverse_linear line 124
10. lemma OAI.MaximalSeshadri.FormalCoordinates.constantCoeff_equiv line 176
11. lemma OAI.MaximalSeshadri.AlgebraicJets.exists_standardized_formalTaylor line 205
12. theorem OAI.MaximalSeshadri.AlgebraicJets.fullRankTaylor_localJet_kernel line 240
13. theorem OAI.MaximalSeshadri.AlgebraicJets.fullRankTaylor_surjective_localJet line 259