OAI/NumberTheory/PiExponent/Geometry/WeightedLocalSheaf.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.WeightedLocalSheaf.monomialSheaf line 16
  2. def OAI.PiExponent.WeightedLocalSheaf.monomialFrame line 22
  3. def OAI.PiExponent.WeightedLocalSheaf.monomialLineBundle line 31
  4. def OAI.PiExponent.WeightedLocalSheaf.monomialSectionMap line 42
  5. def OAI.PiExponent.WeightedLocalSheaf.monomialSection line 51
  6. def OAI.PiExponent.WeightedLocalSheaf.generatedSheaf line 59
  7. def OAI.PiExponent.WeightedLocalSheaf.generatedSectionMap line 64
  8. theorem OAI.PiExponent.WeightedLocalSheaf.generatedSectionMap_bijective_of_span line 72
  9. def OAI.PiExponent.WeightedLocalSheaf.generatedSection line 89
  10. theorem OAI.PiExponent.WeightedLocalSheaf.generatedSection_isIso_of_minimum line 96
  11. def OAI.PiExponent.WeightedLocalSheaf.generatedLineBundle line 109