OAI/AlgebraicGeometry/SurfaceCones/GlobalBaseChange.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Closed base change between the zero sections, obtained from the canonical affine mates by pasting and descent along the affine cover.

  1. lemma OAI.SourcePullbackChart.completedClosedChart_mate_isIso line 20
  2. lemma OAI.SourcePullbackChart.open_pullback_qc line 27
  3. lemma OAI.SourcePullbackChart.actualMate_chart_isIso line 32
  4. lemma OAI.SourcePullbackChart.actualMate_isIso line 61
  5. def OAI.SourcePullbackChart.actualClosedBaseChangeIso line 81