OAI/AlgebraicGeometry/LogKodaira/Adjunction.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ReverseLogKodaira.CanonicalAdjunction.BaseDifferentials line 13
  2. lemma OAI.ReverseLogKodaira.CanonicalAdjunction.alternating_basis_formula line 20
  3. def OAI.ReverseLogKodaira.CanonicalAdjunction.determinantCoordinate line 32
  4. lemma OAI.ReverseLogKodaira.CanonicalAdjunction.determinantCoordinate_wedge line 48
  5. lemma OAI.ReverseLogKodaira.CanonicalAdjunction.split_coprod_bijective line 62
  6. def OAI.ReverseLogKodaira.CanonicalAdjunction.splitEquiv line 83
  7. lemma OAI.ReverseLogKodaira.CanonicalAdjunction.splitEquiv_apply line 86
  8. lemma OAI.ReverseLogKodaira.CanonicalAdjunction.splitEquiv_symm_snd line 89
  9. lemma OAI.ReverseLogKodaira.CanonicalAdjunction.splitEquiv_symm_f line 95
  10. def OAI.ReverseLogKodaira.CanonicalAdjunction.adaptedBasis line 103
  11. lemma OAI.ReverseLogKodaira.CanonicalAdjunction.adaptedBasis_det line 106
  12. def OAI.ReverseLogKodaira.CanonicalAdjunction.splitDeterminantEquiv line 129
  13. lemma OAI.ReverseLogKodaira.CanonicalAdjunction.splitDeterminantEquiv_wedge line 136
  14. theorem OAI.ReverseLogKodaira.CanonicalAdjunction.exact_canonical_adjunction line 154
  15. theorem OAI.ReverseLogKodaira.CanonicalAdjunction.smooth_canonical_adjunction line 171