OAI/RepresentationTheory/RestrictedTilting/DualSplitting.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Standard-costandard extension splitting and dual rational representations.

  1. lemma OAI.FiberFunctorProof.standard_weight_bound line 18
  2. lemma OAI.FiberFunctorProof.hasWeightsBetween_mono line 29
  3. theorem OAI.FiberFunctorProof.standard_costandard_split_of_le line 38
  4. def OAI.FiberFunctorProof.inverseCoordinatePolynomial line 72
  5. lemma OAI.FiberFunctorProof.eval_inverseCoordinatePolynomial line 77
  6. lemma OAI.FiberFunctorProof.IsRational.dual line 85
  7. lemma OAI.FiberFunctorProof.dual_intertwines line 101
  8. lemma OAI.FiberFunctorProof.eval_intertwines line 112
  9. lemma OAI.FiberFunctorProof.equivariant_section_of_retraction line 129
  10. lemma OAI.FiberFunctorProof.equivariant_retraction_of_dual_section line 160
  11. lemma OAI.FiberFunctorProof.dual_sequence_exact line 193
  12. lemma OAI.FiberFunctorProof.dual_eval_intertwines line 203
  13. theorem OAI.FiberFunctorProof.standard_costandard_split line 225
  14. lemma OAI.FiberFunctorProof.IsRational.of_injective line 266
  15. lemma OAI.FiberFunctorProof.IsRational.of_surjective line 279
  16. lemma OAI.FiberFunctorProof.regular_linearChange_coeff line 295
  17. lemma OAI.FiberFunctorProof.costandard_rational line 325