OAI/AlgebraicGeometry/LogKodaira/GlobalSpecialization.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReverseLogKodaira.DifferentialBaseChange.degreeTransport line 16
2. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.logarithmicPullback_degreeTransport line 22
3. structure OAI.ReverseLogKodaira.FiberChartSpecialization.NumeratorChart line 39
4. def OAI.ReverseLogKodaira.FiberChartSpecialization.NumeratorChart.value line 73
5. lemma OAI.ReverseLogKodaira.FiberChartSpecialization.fiber_point_image line 86
6. lemma OAI.ReverseLogKodaira.FiberChartSpecialization.fiber_dimension_eq line 93
7. lemma OAI.ReverseLogKodaira.FiberChartSpecialization.local_logarithmic_numerator line 112
8. lemma OAI.ReverseLogKodaira.FiberChartSpecialization.NumeratorChart.exists_near_fiber_point line 135
9. lemma OAI.ReverseLogKodaira.FiberChartSpecialization.NumeratorChart.value_eq_of_refinement line 181
10. lemma OAI.ReverseLogKodaira.FiberChartSpecialization.NumeratorChart.value_eq line 201
11. theorem OAI.ReverseLogKodaira.FiberChartSpecialization.exists_global_specialization line 231