OAI/Algebra/AlgebraicObstruction/SemilocalCompletion.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.map_map_equiv line 13
2. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.AdicFunctor.equiv line 23
3. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PolynomialPointCompletion.shift line 37
4. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PolynomialPointCompletion.vars_ker line 42
5. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PolynomialPointCompletion.constant_shift line 56
6. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PolynomialPointCompletion.completionEquiv line 65
7. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PolynomialPointCompletion.isDomain_completion line 77
8. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.algebraMapCompletion line 89
9. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorHom line 95
10. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorHom_eq line 103
11. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionScalar.tensorAlgEquiv line 112
12. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.pow_iInf line 125
13. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.level line 135
14. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.level_mk line 141
15. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.level_factor line 145
16. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.forward line 152
17. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.eval_to line 157
18. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.inverseFamily line 167
19. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.inverseFamily_compatible line 173
20. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.inverse line 186
21. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.eval_inverse line 190
22. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.equiv line 196
23. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.CompletionCRT.reduced_factor line 215
24. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PowerCofinal.family line 240
25. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PowerCofinal.compatible line 245
26. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PowerCofinal.map line 254
27. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PowerCofinal.eval_map line 258
28. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PowerCofinal.map_map line 264
29. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PowerCofinal.equiv line 275
30. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.PowerCofinal.radicalEquiv line 283
31. def OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.SemilocalCompletion.primes line 301
32. instance OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.SemilocalCompletion.primesMaximal line 304
33. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.SemilocalCompletion.primes_pairwise line 308
34. lemma OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.SemilocalCompletion.iInf_primes line 319
35. theorem OAI.BoundaryOnly.FormalObstruction.AlgebraicReplacement.SemilocalCompletion.reduced_at_maximal line 326