OAI/AlgebraicGeometry/LogKodaira/RelativeCanonical.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReverseLogKodaira.RelativeCanonical.relativeCanonicalEquiv line 17
2. lemma OAI.ReverseLogKodaira.RelativeCanonical.relativeCanonicalEquiv_wedge line 29
3. lemma OAI.ReverseLogKodaira.RelativeCanonical.relative_canonical_ext line 50
4. lemma OAI.ReverseLogKodaira.RelativeCanonical.differential_map_tower line 83
5. lemma OAI.ReverseLogKodaira.RelativeCanonical.differential_map_relative line 98
6. theorem OAI.ReverseLogKodaira.RelativeCanonical.relative_canonical_naturality line 116
7. lemma OAI.ReverseLogKodaira.BasedRelativeCanonical.formallySmooth_mapBaseChange_injective line 153
8. def OAI.ReverseLogKodaira.BasedRelativeCanonical.basedAdjunction line 168
9. def OAI.ReverseLogKodaira.BasedRelativeCanonical.basedRelativeCanonicalEquiv line 182
10. lemma OAI.ReverseLogKodaira.BasedRelativeCanonical.basedAdjunction_wedge line 199
11. lemma OAI.ReverseLogKodaira.BasedRelativeCanonical.basedRelativeCanonicalEquiv_general_wedge line 216
12. lemma OAI.ReverseLogKodaira.BasedRelativeCanonical.basedRelativeCanonicalEquiv_wedge line 231
13. lemma OAI.ReverseLogKodaira.BasedRelativeCanonical.based_relative_canonical_ext line 249
14. theorem OAI.ReverseLogKodaira.BasedRelativeCanonical.based_relative_canonical_naturality line 283