OAI/Algebra/AlgebraicObstruction/ArcDetection.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.radical_eq_maximal_of_minimal line 14
2. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.exists_primary_curve_quotient line 26
3. instance OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.quotient_localRing line 102
4. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.local_quotient_complete line 109
5. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.quotient_residue_surjective line 131
6. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.domain_detecting_arc line 163
7. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.reduced_detecting_arc line 197
8. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.reduced_detecting_continuous_arc line 231
9. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.polynomial_approximate line 252
10. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.span_variables_eq_constant_kernel line 281
11. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.maximalIdeal_eq_variables line 317
12. instance OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.complete_mps_maximal line 325
13. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.residue_mps_surjective line 330
14. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.FormalArc.local_mps_hom_ext line 340