OAI/Algebra/AlgebraicObstruction/ChartCompletion.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.truncatedEquiv_compatible line 16
2. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionFamily line 28
3. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionFamily_compatible line 34
4. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionToPolynomial line 43
5. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.eval_completionToPolynomial line 48
6. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.variables_le_comap_maximal line 55
7. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.polynomialToCompletion line 61
8. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.quotient_polynomial line 67
9. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.eval_polynomialToCompletion line 75
10. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionToPolynomial_polynomialToCompletion line 81
11. lemma OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.polynomialToCompletion_completionToPolynomial line 89
12. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.polynomialCompletionEquiv line 97
13. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionEquiv line 105
14. theorem OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionEquiv_of line 110
15. def OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.completionAlgEquiv line 122
16. instance OAI.BoundaryOnly.FormalObstruction.FormalCorrection.AffineEtaleChart.localNoetherian line 127