OAI/AlgebraicGeometry/NumericalDimension/TwistedPushforward.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Twisted Pushforward.

  1. def OAI.NumericalDimensionOne.twistedToRoundupFunction line 42
  2. def OAI.NumericalDimensionOne.twistedToRoundupLinear line 63
  3. def OAI.NumericalDimensionOne.twistedToRoundupBilinear line 96
  4. def OAI.NumericalDimensionOne.twistedToRoundupApp line 123
  5. def OAI.NumericalDimensionOne.twistedToRoundupPresheaf line 137
  6. lemma OAI.NumericalDimensionOne.divisorSectionOn_div_equation line 186
  7. lemma OAI.NumericalDimensionOne.divisorFunctionLocal_div_equation line 202
  8. lemma OAI.NumericalDimensionOne.divisorFunctionLocal_mul_equation line 222
  9. def OAI.NumericalDimensionOne.divisorPushforwardShiftEquiv line 243
  10. lemma OAI.NumericalDimensionOne.twistedToRoundupApp_bijective_on_chart line 313
  11. def OAI.NumericalDimensionOne.moduleStalkMap line 381
  12. lemma OAI.NumericalDimensionOne.moduleStalkMap_germ line 385
  13. lemma OAI.NumericalDimensionOne.moduleStalkMap_smul_germ line 390
  14. def OAI.NumericalDimensionOne.moduleStalkLinearMap line 397
  15. theorem OAI.NumericalDimensionOne.moduleStalkMap_bijective_of_local line 439
  16. def OAI.NumericalDimensionOne.twistedToRoundup line 494
  17. lemma OAI.NumericalDimensionOne.twistedToRoundup_fac line 500
  18. lemma OAI.NumericalDimensionOne.twistedToRoundupPresheaf_stalk_bijective line 561
  19. lemma OAI.NumericalDimensionOne.twistedToRoundup_stalk_bijective line 587
  20. theorem OAI.NumericalDimensionOne.twistedMultiplierModuleSheaf_iso_pushforward_on_snc_model line 641