OAI/AlgebraicGeometry/LogKodaira/BaseChange.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ReverseLogKodaira.DifferentialBaseChange.alternatingRestriction line 18
  2. def OAI.ReverseLogKodaira.DifferentialBaseChange.exteriorScalarMap line 22
  3. def OAI.ReverseLogKodaira.DifferentialBaseChange.tensorScalarMap line 26
  4. abbrev OAI.ReverseLogKodaira.DifferentialBaseChange.Canonical line 37
  5. abbrev OAI.ReverseLogKodaira.DifferentialBaseChange.Pluricanonical line 38
  6. def OAI.ReverseLogKodaira.DifferentialBaseChange.exteriorDifferentialMap line 40
  7. def OAI.ReverseLogKodaira.DifferentialBaseChange.pluricanonicalMap line 43
  8. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.lift_bijective_of_basis line 53
  9. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.exteriorScalarMap_wedge line 64
  10. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.exterior_bijective_of_basis line 71
  11. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.tensor_bijective_of_basis line 82
  12. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.tensorKaehlerEquiv_tmul line 104
  13. theorem OAI.ReverseLogKodaira.DifferentialBaseChange.smooth_pluricanonical_baseChange line 117