OAI/RepresentationTheory/RestrictedTilting/LatticeGluing.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Free intersections, power localizations and finite glued lattices.

  1. lemma OAI.FiberFunctorProof.tensor_span_pair line 16
  2. theorem OAI.FiberFunctorProof.free_of_two_generators line 39
  3. theorem OAI.FiberFunctorProof.intersection_regular line 85
  4. theorem OAI.FiberFunctorProof.intersection_free line 113
  5. def OAI.FiberFunctorProof.powerLocalization line 131
  6. lemma OAI.FiberFunctorProof.le_powerLocalization line 145
  7. lemma OAI.FiberFunctorProof.powerLocalization_mono line 149
  8. lemma OAI.FiberFunctorProof.powerLocalization_div line 160
  9. def OAI.FiberFunctorProof.coordinateMap line 174
  10. def OAI.FiberFunctorProof.coordinateLattice line 179
  11. lemma OAI.FiberFunctorProof.mem_coordinateLattice line 182
  12. instance OAI.FiberFunctorProof.coordinateLattice_finite line 191
  13. theorem OAI.FiberFunctorProof.coordinateLattice_intersection line 197
  14. def OAI.FiberFunctorProof.gluedLattice line 234
  15. lemma OAI.FiberFunctorProof.gluedLattice_bound line 240
  16. theorem OAI.FiberFunctorProof.gluedLattice_finite line 261
  17. theorem OAI.FiberFunctorProof.gluedLattice_free line 285