OAI/AlgebraicGeometry/RelativeTriviality/IsomorphismLocus.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CampanaPeternellSix.RelativeCech.isoLocus line 14
2. lemma OAI.CampanaPeternellSix.RelativeCech.mem_isoLocus line 16
3. lemma OAI.CampanaPeternellSix.RelativeCech.isIso_of_local_bijective line 20
4. lemma OAI.CampanaPeternellSix.RelativeCech.isIso_restrict_of_range_in_isoLocus line 44
5. lemma OAI.CampanaPeternellSix.RelativeCech.isIso_pullback_isoLocus line 56
6. lemma OAI.CampanaPeternellSix.RelativeCech.isIso_pullback_of_range_in_isoLocus line 66
7. lemma OAI.CampanaPeternellSix.RelativeCech.affine_field_point_mem_isoLocus line 86
8. lemma OAI.CampanaPeternellSix.RelativeCech.mem_isoLocus_of_mem_restrict line 109
9. lemma OAI.CampanaPeternellSix.RelativeCech.flat_affine_sections line 136
10. lemma OAI.CampanaPeternellSix.RelativeCech.finitePresentation_affine_sections line 142
11. lemma OAI.CampanaPeternellSix.RelativeCech.field_point_mem_isoLocus line 154
12. lemma OAI.CampanaPeternellSix.RelativeCech.exists_basicOpen_preimage_le line 199
13. lemma OAI.CampanaPeternellSix.RelativeCech.residueSpecMap_apply line 219
14. lemma OAI.CampanaPeternellSix.RelativeCech.fiber_mem_isoLocus line 226
15. lemma OAI.CampanaPeternellSix.RelativeCech.isIso_near_fiber_proper line 253