OAI/RepresentationTheory/RestrictedTilting/JetRepresentations.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Plane jet modules, homogeneous layers and equivariant inclusions.

  1. abbrev OAI.FiberFunctorProof.planeJetRelation line 20
  2. def OAI.FiberFunctorProof.jetMonomialBasis line 23
  3. lemma OAI.FiberFunctorProof.jetMonomialBasis_apply line 27
  4. lemma OAI.FiberFunctorProof.homogeneous_smul_mem_jet line 34
  5. lemma OAI.FiberFunctorProof.homogeneous_smul_pair_mem_next line 49
  6. def OAI.FiberFunctorProof.PlaneCompatible line 71
  7. lemma OAI.FiberFunctorProof.planeJetRelation_stable line 75
  8. def OAI.FiberFunctorProof.planeJetRep line 91
  9. lemma OAI.FiberFunctorProof.planeJetRep_mk line 96
  10. lemma OAI.FiberFunctorProof.planeJetRep_rational line 101
  11. abbrev OAI.FiberFunctorProof.planeJetLayerRelation line 109
  12. abbrev OAI.FiberFunctorProof.planeJetLayer line 111
  13. def OAI.FiberFunctorProof.planeHomogeneousMultiply line 113
  14. def OAI.FiberFunctorProof.planeLayerMul line 119
  15. lemma OAI.FiberFunctorProof.planeLayerMul_ker line 123
  16. def OAI.FiberFunctorProof.planeLayerBilinear line 128
  17. def OAI.FiberFunctorProof.planeLayerMultiply line 150
  18. lemma OAI.FiberFunctorProof.planeLayerMultiply_tmul_mk line 155
  19. lemma OAI.FiberFunctorProof.planeLayerMultiply_sum line 160
  20. lemma OAI.FiberFunctorProof.tensor_basis_decomposition line 170
  21. lemma OAI.FiberFunctorProof.planeLayerMultiply_surjective line 187
  22. lemma OAI.FiberFunctorProof.planeLayerMultiply_injective line 193
  23. def OAI.FiberFunctorProof.planeLayerEquiv line 219
  24. def OAI.FiberFunctorProof.planeJetSubrep line 229
  25. lemma OAI.FiberFunctorProof.planeJetLayerRelation_stable line 234
  26. def OAI.FiberFunctorProof.planeJetLayerRep line 241
  27. lemma OAI.FiberFunctorProof.planeLayerMultiply_intertwines line 247
  28. lemma OAI.FiberFunctorProof.planeLayer_finite line 267
  29. lemma OAI.FiberFunctorProof.planeJetRelation_succ_le line 271
  30. lemma OAI.FiberFunctorProof.planeJetRelation_zero line 275
  31. def OAI.FiberFunctorProof.planeJetTransition line 278
  32. lemma OAI.FiberFunctorProof.planeJetTransition_mk line 283
  33. lemma OAI.FiberFunctorProof.planeJetTransition_surjective line 287
  34. def OAI.FiberFunctorProof.planeJetLayerInclusion line 293
  35. lemma OAI.FiberFunctorProof.planeJetLayerInclusion_mk line 300
  36. lemma OAI.FiberFunctorProof.planeJetLayerInclusion_injective line 304
  37. lemma OAI.FiberFunctorProof.planeJet_shortExact line 315
  38. lemma OAI.FiberFunctorProof.planeJet_finite line 328
  39. lemma OAI.FiberFunctorProof.planeJetTransition_intertwines line 339
  40. lemma OAI.FiberFunctorProof.planeJetLayerInclusion_intertwines line 347