OAI/Algebra/AlgebraicObstruction/EtaleCharts.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart line 14
2. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.base line 25
3. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.prod line 32
4. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.range_left line 41
5. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.range_right line 47
6. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.LocalEtaleExpansion.affine line 53
7. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.common_affine_chart line 81
8. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.coordinate_series_flat line 104
9. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.etale_expansion_faithfullyFlat line 109
10. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.etale_expansion_mem_iff line 124
11. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.point line 148
12. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.(instance at line 151) line 151
13. abbrev OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.LocalRing line 153
14. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.outside_point_unit line 156
15. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localExpansion line 161
16. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localExpansion_map line 165
17. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localExpansion_isLocalHom line 169
18. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localAlgebra line 180
19. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localTower line 183
20. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localAlgebra_isLocalHom line 187
21. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localEssFiniteType line 191
22. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localFormallyEtale line 195
23. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localFaithfullyFlat line 198
24. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localRange line 202
25. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localGerm line 207