OAI/AlgebraicGeometry/LogKodaira/FiberCharts.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReverseLogKodaira.FiberChartSpecialization.logarithmicNumerator line 17
2. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.fiber_affine_chart_pushout line 55
3. lemma OAI.ReverseLogKodaira.CanonicalSpecialization.exterior_fiber_target_tower line 98
4. lemma OAI.ReverseLogKodaira.CanonicalSpecialization.specialization_target_tower line 122
5. theorem OAI.ReverseLogKodaira.FiberChartSpecialization.local_specialization_regular line 158
6. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.chartToFunctionField_restrict line 231
7. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.constants_restrict line 249
8. theorem OAI.ReverseLogKodaira.FiberChartSpecialization.specialization_refinement line 266