OAI/AlgebraicGeometry/LogKodaira/Specialization.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReverseLogKodaira.CanonicalSpecialization.specializeCanonical line 13
2. def OAI.ReverseLogKodaira.CanonicalSpecialization.specializePluricanonical line 27
3. lemma OAI.ReverseLogKodaira.CanonicalSpecialization.differential_map_fiber_tower line 44
4. lemma OAI.ReverseLogKodaira.CanonicalSpecialization.exterior_map_fiber_tower line 62
5. lemma OAI.ReverseLogKodaira.CanonicalSpecialization.canonical_specialization_naturality line 79
6. theorem OAI.ReverseLogKodaira.CanonicalSpecialization.pluricanonical_specialization_naturality line 108
7. lemma OAI.ReverseLogKodaira.FractionalCanonical.exists_absolute_basis line 145
8. lemma OAI.ReverseLogKodaira.FractionalCanonical.free_pluricanonical_injective line 159
9. theorem OAI.ReverseLogKodaira.FractionalCanonical.based_pluricanonical_injective line 203
10. def OAI.ReverseLogKodaira.LogarithmicSpecialization.logarithmicPullback line 222
11. def OAI.ReverseLogKodaira.LogarithmicSpecialization.logarithmicSpecialize line 230
12. lemma OAI.ReverseLogKodaira.LogarithmicSpecialization.pluricanonical_map_tower line 247
13. lemma OAI.ReverseLogKodaira.LogarithmicSpecialization.logarithmicPullback_naturality line 267
14. lemma OAI.ReverseLogKodaira.LogarithmicSpecialization.logarithmicSpecialize_naturality line 280
15. lemma OAI.ReverseLogKodaira.LogarithmicSpecialization.logarithmicPullback_injective line 302
16. theorem OAI.ReverseLogKodaira.LogarithmicSpecialization.logarithmic_specialization_chart_independent line 318
17. theorem OAI.ReverseLogKodaira.LogarithmicSpecialization.logarithmic_specialization_equation_independent line 352