OAI/AlgebraicGeometry/LogKodaira/Descent.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ReverseLogKodaira.PluriformDescent.absolutePluriformCoordinate line 15
2. def OAI.ReverseLogKodaira.PluriformDescent.BaseVanishesAt line 23
3. def OAI.ReverseLogKodaira.PluriformDescent.FiberVanishesAt line 37
4. def OAI.ReverseLogKodaira.PluriformDescent.SectionConstructionStatement line 52
5. theorem OAI.ReverseLogKodaira.FiberIdeal.ker_inl_of_surjective line 73
6. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.fiber_chart_kernel line 115
7. theorem OAI.ReverseLogKodaira.FiberChartSpecialization.original_frame_coefficient_mem_fiber_ideal line 148
8. theorem OAI.ReverseLogKodaira.PluriformDescent.original_coefficient_in_point_ideal_of_fiber_zero line 197