OAI/AlgebraicGeometry/Seshadri/Jets/FormalAdic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MaximalSeshadri.FormalAdic.completion_eval_kernel line 15
  2. lemma OAI.MaximalSeshadri.FormalAdic.trunc_eq_completion_eval line 29
  3. lemma OAI.MaximalSeshadri.FormalAdic.polynomials_map_vars line 46
  4. lemma OAI.MaximalSeshadri.FormalAdic.trunc_kernel line 60
  5. lemma OAI.MaximalSeshadri.FormalAdic.maximalIdeal_eq_ker_constantCoeff line 79
  6. lemma OAI.MaximalSeshadri.FormalAdic.maximalIdeal_eq_vars line 86
  7. lemma OAI.MaximalSeshadri.FormalAdic.trunc_kernel_maximalIdeal line 103
  8. lemma OAI.MaximalSeshadri.LocalComparison.comap_extension_sup line 116
  9. lemma OAI.MaximalSeshadri.LocalComparison.adicClosed line 127
  10. theorem OAI.MaximalSeshadri.LocalComparison.contractExtension line 148
  11. lemma OAI.MaximalSeshadri.LocalComparison.quotientMap_surjective_of_finiteJet line 164
  12. def OAI.MaximalSeshadri.LocalComparison.quotientEquiv line 178
  13. theorem OAI.MaximalSeshadri.LocalComparison.colength_eq line 192
  14. lemma OAI.MaximalSeshadri.LocalComparison.exists_pow_le_of_finite line 202
  15. def OAI.MaximalSeshadri.LocalComparison.finiteQuotientEquiv line 219
  16. lemma OAI.MaximalSeshadri.LocalComparison.localizedJet_kernel line 238
  17. lemma OAI.MaximalSeshadri.LocalComparison.localizedJet_surjective line 256
  18. lemma OAI.MaximalSeshadri.LocalComparison.image_primeCompl_isUnit line 268
  19. def OAI.MaximalSeshadri.LocalComparison.localTaylorLift line 277
  20. lemma OAI.MaximalSeshadri.LocalComparison.localTaylorLift_comp line 284