OAI/AlgebraicGeometry/LogKodaira/LatticeBaseChange.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.exterior_span_of_span line 16
2. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.tensor_span_of_span line 31
3. theorem OAI.ReverseLogKodaira.DifferentialBaseChange.formallyEtale_pluricanonical_span line 51
4. def OAI.ReverseLogKodaira.DifferentialBaseChange.rationalLattice line 79
5. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.span_wedges line 90
6. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.pluri_symbol line 107
7. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.range_pluricanonicalMap line 119
8. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.differential_map_fiber_tower line 140
9. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.exterior_map_fiber_tower line 158
10. lemma OAI.ReverseLogKodaira.DifferentialBaseChange.pluricanonical_map_tower line 175
11. theorem OAI.ReverseLogKodaira.DifferentialBaseChange.rationalLattice_formallyEtale line 197