OAI/AlgebraicGeometry/RelativeTriviality/AffineSquare.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CampanaPeternellSix.AffineSquare.section_square_unit line 18
  2. def OAI.CampanaPeternellSix.AffineSquare.pushforwardSquare line 29
  3. def OAI.CampanaPeternellSix.AffineSquare.squareAdjunction line 33
  4. def OAI.CampanaPeternellSix.AffineSquare.restrictionPullbackIso line 37
  5. lemma OAI.CampanaPeternellSix.AffineSquare.restrictionPullbackIso_unit line 42
  6. lemma OAI.CampanaPeternellSix.AffineSquare.comparison_unit line 49
  7. lemma OAI.CampanaPeternellSix.AffineSquare.restriction_maps_comp line 75
  8. lemma OAI.CampanaPeternellSix.AffineSquare.restriction_unit_top line 84
  9. lemma OAI.CampanaPeternellSix.AffineSquare.comparison_unit_top line 92
  10. def OAI.CampanaPeternellSix.AffineSquare.sectionMap line 140
  11. lemma OAI.CampanaPeternellSix.AffineSquare.image_top_le_preimage line 147
  12. lemma OAI.CampanaPeternellSix.AffineSquare.sectionMap_apply line 153
  13. lemma OAI.CampanaPeternellSix.AffineSquare.isBaseChange_sections line 164
  14. lemma OAI.CampanaPeternellSix.RelativeCech.isBaseChange_restrictScalars line 202
  15. lemma OAI.CampanaPeternellSix.AffineSquare.isBaseChange_sections_overBase line 225
  16. lemma OAI.CampanaPeternellSix.AffineSquare.appTop_appIso_inv line 281
  17. lemma OAI.CampanaPeternellSix.AffineSquare.scalar_identity line 287
  18. def OAI.CampanaPeternellSix.AffineSquare.coefficientSectionEquiv line 296
  19. abbrev OAI.CampanaPeternellSix.AffineSquare.coefficientModule line 330
  20. lemma OAI.CampanaPeternellSix.AffineSquare.scalar_section_map line 335
  21. def OAI.CampanaPeternellSix.AffineSquare.coefficientUnit line 346
  22. lemma OAI.CampanaPeternellSix.AffineSquare.coefficientUnit_isBaseChange line 392
  23. lemma OAI.CampanaPeternellSix.AffineSquare.coefficientUnit_isBaseChange_of_image line 429
  24. def OAI.CampanaPeternellSix.AffineSquare.baseScalars line 452
  25. def OAI.CampanaPeternellSix.AffineSquare.openBaseScalars line 454
  26. lemma OAI.CampanaPeternellSix.AffineSquare.baseScalars_natural line 458
  27. lemma OAI.CampanaPeternellSix.AffineSquare.openBaseScalars_pushout line 464
  28. lemma OAI.CampanaPeternellSix.AffineSquare.fromSpec_appTop line 492
  29. lemma OAI.CampanaPeternellSix.AffineSquare.coefficientUnit_isBaseChange_of_isPushout line 509
  30. lemma OAI.CampanaPeternellSix.AffineSquare.coefficientUnit_naturality line 551