OAI/AlgebraicGeometry/SurfaceCones/ClosedChartBaseChange.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Closed base change on the completed source charts.

  1. def OAI.SourcePullbackChart.completedClosedChartBaseChangeIso line 19
  2. def OAI.AffineClosedBaseChange.moduleRightIso line 38
  3. lemma OAI.AffineClosedBaseChange.moduleRightIso_apply line 45
  4. def OAI.AffineClosedBaseChange.moduleMate line 48
  5. lemma OAI.AffineClosedBaseChange.moduleMate_one_tmul line 55
  6. lemma OAI.AffineClosedBaseChange.moduleMate_eq line 75
  7. instance OAI.AffineClosedBaseChange.moduleMate_app_isIso line 107
  8. instance OAI.AffineClosedBaseChange.moduleMate_isIso line 111
  9. def OAI.ActualSheafBaseChange.rightIso line 126
  10. def OAI.ActualSheafBaseChange.mate line 129
  11. lemma OAI.ActualSheafBaseChange.mate_unit line 133
  12. lemma OAI.ActualSheafBaseChange.mate_eq_iff line 141
  13. lemma OAI.AffineClosedBaseChange.rotate_iso_square line 160
  14. lemma OAI.AffineClosedBaseChange.spec_square line 169
  15. lemma OAI.AffineClosedBaseChange.gamma_cube line 172
  16. lemma OAI.AffineClosedBaseChange.gamma_cube_inv line 194
  17. def OAI.AdjunctionBCUnit.leftIso line 237
  18. def OAI.AdjunctionBCUnit.pushComparison line 240
  19. lemma OAI.AdjunctionBCUnit.unit_pushComparison line 243
  20. lemma OAI.AdjunctionBCUnit.pushComparison_naturality line 248
  21. lemma OAI.AdjunctionBCUnit.unit_comparison line 262
  22. lemma OAI.AffinePullback.pushComparison_eq line 295
  23. lemma OAI.AffinePullback.pullbackTildeIso_unit line 304
  24. lemma OAI.AffinePullback.pushforwardTildeIso_inv_unit line 315
  25. lemma OAI.AffinePullback.pushforwardTildeIso_inv_naturality line 325
  26. lemma OAI.AffinePullback.gamma_pushTilde_comp line 334
  27. lemma OAI.AffineClosedBaseChange.push_cube line 361
  28. lemma OAI.AffineClosedBaseChange.moduleMate_unit line 423
  29. lemma OAI.AffineClosedBaseChange.tildeMate_eq line 434
  30. instance OAI.AffineClosedBaseChange.tildeMate_isIso line 505
  31. instance OAI.AffineClosedBaseChange.sheafMate_isIso line 511
  32. def OAI.ActualMateTransport.left₁ line 535
  33. def OAI.ActualMateTransport.left₂ line 536
  34. def OAI.ActualMateTransport.square line 538
  35. lemma OAI.ActualMateTransport.square_refl line 541
  36. lemma OAI.ActualMateTransport.mate_transport line 546
  37. lemma OAI.ActualMateTransport.mate_transport_app line 556
  38. lemma OAI.ActualMateTransport.mate_transport_isIso line 564
  39. lemma OAI.ActualMateTransport.mate_transport_isIso_iff line 579
  40. lemma OAI.ActualSheafBaseChange.restrictMate_eq line 595
  41. instance OAI.ActualSheafBaseChange.openMate_isIso line 604
  42. lemma OAI.ActualMatePasting.mate_app line 639
  43. lemma OAI.ActualMatePasting.mate_hcomp line 648
  44. lemma OAI.ActualMatePasting.mate_hcomp_app line 655
  45. lemma OAI.ActualMatePasting.mate_hcomp_isIso line 664
  46. lemma OAI.ActualMatePasting.map_mate_isIso line 670
  47. lemma OAI.ActualSheafBaseChange.restrict_map_app line 694
  48. def OAI.ActualSheafBaseChange.restrictMate line 697
  49. lemma OAI.ActualSheafBaseChange.restrictMate_app_app line 701
  50. lemma OAI.ActualSheafBaseChange.restrictMate_isIso line 713
  51. lemma OAI.ActualSheafBaseChange.openCartesianMate_isIso line 723
  52. lemma OAI.ActualSheafBaseChange.paste_comm line 751
  53. def OAI.ActualSheafBaseChange.square line 754
  54. lemma OAI.ActualSheafBaseChange.right_square_paste line 756
  55. lemma OAI.ActualSheafBaseChange.pasted_mate_isIso line 778
  56. lemma OAI.ActualSheafBaseChange.mate_isIso_congr line 803
  57. lemma OAI.ActualSheafBaseChange.map_mate_of_pasted_isIso line 808