OAI/RepresentationTheory/RestrictedTilting/AssociatedLattices.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Associated-origin finiteness, lattice equivalence and numerator evaluations.

  1. lemma OAI.FiberFunctorProof.associatedCoordinate_smul line 20
  2. lemma OAI.FiberFunctorProof.associatedOrigin_coordinate_mem line 33
  3. theorem OAI.FiberFunctorProof.associatedOrigin_finite line 42
  4. lemma OAI.FiberFunctorProof.planeChartToFraction_invSelf line 57
  5. lemma OAI.FiberFunctorProof.planeChartVector_exists line 69
  6. lemma OAI.FiberFunctorProof.planeOverlapToFraction_injective line 83
  7. lemma OAI.FiberFunctorProof.planeChartPair_evaluation_relation line 99
  8. def OAI.FiberFunctorProof.associatedLatticeMap line 134
  9. lemma OAI.FiberFunctorProof.associatedLatticeMap_surjective line 140
  10. def OAI.FiberFunctorProof.associatedLatticeEquiv line 171
  11. lemma OAI.FiberFunctorProof.associatedFractionChart_apply line 181
  12. lemma OAI.FiberFunctorProof.associatedNumerator_exists line 186
  13. lemma OAI.FiberFunctorProof.associatedNumerator_evaluation line 205