OAI/NumberTheory/PiExponent/Approximation/CoherentTwistPresentation.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PiExponent.CoherentTwist.affineSections line 15
  2. abbrev OAI.PiExponent.CoherentTwist.principalRestriction line 18
  3. theorem OAI.PiExponent.CoherentTwist.principalRestriction_localizes line 21
  4. theorem OAI.PiExponent.CoherentTwist.principal_section_extends line 25
  5. theorem OAI.PiExponent.CoherentTwist.principal_section_zero line 35
  6. theorem OAI.PiExponent.CoherentTwist.finite_principal_sections_extend line 45
  7. theorem OAI.PiExponent.CoherentTwist.finite_principal_sections_zero line 57
  8. lemma OAI.PiExponent.CoherentTwist.app_zero_of_restrict line 69
  9. lemma OAI.PiExponent.CoherentTwist.eq_zero_of_local line 82
  10. lemma OAI.PiExponent.CoherentTwist.epi_of_local line 103
  11. lemma OAI.PiExponent.CoherentTwist.mono_of_local line 116
  12. lemma OAI.PiExponent.CoherentTwist.exact_of_local line 129
  13. lemma OAI.PiExponentSeshadri.Geometry.tensorRestrict_natural line 150
  14. lemma OAI.PiExponentSeshadri.Geometry.modulePresheafTensorRestrict_natural_aux line 163
  15. lemma OAI.PiExponentSeshadri.Geometry.modulePresheafTensorRestrict_natural line 187
  16. lemma OAI.PiExponentSeshadri.Geometry.moduleTensorRestrict_natural line 200
  17. def OAI.PiExponentSeshadri.Geometry.moduleTensorRightFunctor line 237
  18. theorem OAI.PiExponentSeshadri.Geometry.moduleTensorIso_hom line 243
  19. theorem OAI.PiExponentSeshadri.Geometry.moduleTensorRightUnit_natural line 247
  20. def OAI.PiExponentSeshadri.Geometry.moduleTensorFrame line 274
  21. theorem OAI.PiExponentSeshadri.Geometry.moduleTensorFrame_natural line 278
  22. def OAI.PiExponentSeshadri.Geometry.moduleTensorRestrictFrame line 293
  23. theorem OAI.PiExponentSeshadri.Geometry.moduleTensorMap_epi line 308
  24. theorem OAI.PiExponentSeshadri.Geometry.moduleTensorMap_mono line 328
  25. instance OAI.PiExponentSeshadri.Geometry.moduleTensorRightFunctor_preservesZero line 348
  26. theorem OAI.PiExponentSeshadri.Geometry.moduleTensorRightFunctor_exact line 362
  27. theorem OAI.PiExponentSeshadri.Geometry.moduleTensorRightFunctor_shortExact line 373
  28. instance OAI.PiExponentSeshadri.Geometry.moduleTensorRightFunctor_additive line 384
  29. def OAI.PiExponentSeshadri.Geometry.moduleTwistFunctor line 404
  30. instance OAI.PiExponentSeshadri.Geometry.moduleTwistFunctor_additive line 408
  31. theorem OAI.PiExponentSeshadri.Geometry.moduleTwistFunctor_add line 416
  32. theorem OAI.PiExponentSeshadri.Geometry.moduleTwistFunctor_shortExact line 428
  33. def OAI.PiExponentSeshadri.Geometry.moduleTensorComm line 438
  34. def OAI.PiExponentSeshadri.Geometry.moduleTwistUnitIso line 445