OAI/NumberTheory/PiExponent/LocalAlgebra/IdealModule.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentSeshadri.IdealModule.unit line 14
  2. def OAI.PiExponentSeshadri.IdealModule.structureMap line 16
  3. lemma OAI.PiExponentSeshadri.IdealModule.structureMap_app line 20
  4. def OAI.PiExponentSeshadri.IdealModule.idealModule line 23
  5. def OAI.PiExponentSeshadri.IdealModule.inclusion line 25
  6. instance OAI.PiExponentSeshadri.IdealModule.(instance at line 28) line 28
  7. def OAI.PiExponentSeshadri.IdealModule.sectionsKernelIso line 30
  8. lemma OAI.PiExponentSeshadri.IdealModule.sectionsKernelIso_inclusion line 39
  9. lemma OAI.PiExponentSeshadri.IdealModule.image_eq_kernel line 52
  10. lemma OAI.PiExponentSeshadri.IdealModule.image_eq_ideal line 68
  11. def OAI.PiExponentSeshadri.IdealModule.closedModule line 79
  12. def OAI.PiExponentSeshadri.IdealModule.closedInclusion line 81
  13. lemma OAI.PiExponentSeshadri.IdealModule.closed_image line 84
  14. lemma OAI.PiExponentSeshadri.IdealModule.isIso_of_affine_app line 88
  15. def OAI.PiExponentSeshadri.IdealModule.multiply line 98
  16. lemma OAI.PiExponentSeshadri.IdealModule.multiply_app line 114
  17. lemma OAI.PiExponentSeshadri.IdealModule.multiply_structure_zero line 117
  18. def OAI.PiExponentSeshadri.IdealModule.equationToIdeal line 128
  19. lemma OAI.PiExponentSeshadri.IdealModule.equationToIdeal_inclusion line 132
  20. lemma OAI.PiExponentSeshadri.IdealModule.equationToIdeal_app line 136
  21. lemma OAI.PiExponentSeshadri.IdealModule.isIso_equationToIdeal line 142
  22. lemma OAI.PiExponentSeshadri.IdealModule.regular_map_flat line 181
  23. lemma OAI.PiExponentSeshadri.IdealModule.restriction_regular line 190
  24. lemma OAI.PiExponentSeshadri.IdealModule.structureMap_epi line 202
  25. theorem OAI.PiExponentSeshadri.IdealModule.closedSequence_exact line 217