OAI/AlgebraicGeometry/RelativeTriviality/AffinePullback.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CampanaPeternellSix.Cotangent.Affine.specGlobalPushforwardIso line 15
2. def OAI.CampanaPeternellSix.Cotangent.Affine.tildePullbackIso line 44
3. def OAI.CampanaPeternellSix.Cotangent.Affine.affinePullbackAdjunction line 51
4. lemma OAI.CampanaPeternellSix.Cotangent.Affine.tildePullbackIso_homEquiv line 55
5. lemma OAI.CampanaPeternellSix.Cotangent.Affine.tilde_homEquiv_apply line 67
6. lemma OAI.CampanaPeternellSix.Cotangent.Affine.affinePullback_homEquiv_apply line 73
7. lemma OAI.CampanaPeternellSix.Cotangent.Affine.extendTilde_homEquiv_apply line 84
8. def OAI.CampanaPeternellSix.AffineBaseChange.sectionMap line 103
9. def OAI.CampanaPeternellSix.AffineBaseChange.globalPullbackIso line 127
10. lemma OAI.CampanaPeternellSix.AffineBaseChange.tilde_unit_comparison line 137
11. lemma OAI.CampanaPeternellSix.AffineBaseChange.sectionMap_naturality line 157
12. lemma OAI.CampanaPeternellSix.AffineBaseChange.counit_top line 165
13. lemma OAI.CampanaPeternellSix.AffineBaseChange.globalPullbackIso_one line 171
14. theorem OAI.CampanaPeternellSix.AffineBaseChange.isBaseChange_sections line 197