OAI/Algebra/FrobeniusObstruction/VanishingIdeals.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.bijective_of_specialFiber line 16
2. def OAI.BoundaryOnly.FormalObstruction.Frobenius.liftInverse line 52
3. instance OAI.BoundaryOnly.FormalObstruction.ThreeParameters.parameterNontrivial line 67
4. instance OAI.BoundaryOnly.FormalObstruction.ThreeParameters.parameterCharP line 69
5. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.pow_eq_augmentation line 74
6. theorem OAI.BoundaryOnly.FormalObstruction.ThreeParameters.augmentation_zero_pow line 89
7. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.mapCoefficients_algebraMap line 101
8. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.mapCoefficients_smul line 108
9. def OAI.BoundaryOnly.FormalObstruction.Frobenius.baseChange line 121
10. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.baseChange_coordinate line 129
11. def OAI.BoundaryOnly.FormalObstruction.Frobenius.reduction line 139
12. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.reduction_coordinate line 151
13. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.reduction_base line 156
14. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.reduction_baseChange line 161
15. theorem OAI.BoundaryOnly.FormalObstruction.Frobenius.specialFiber_of_coordinates line 170