OAI/Geometry/QuadricBundles/Model.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.QuadricCounterexample.ProjectiveLine line 10

   Also declared: ComparatorChallenges/QuadricBundles.lean:13 (same declaration text).

2. abbrev OAI.QuadricCounterexample.QuadricSurface line 11

   Also declared: ComparatorChallenges/QuadricBundles.lean:14 (same declaration text).

3. def OAI.QuadricCounterexample.reciprocalP1 line 13

   Also declared: ComparatorChallenges/QuadricBundles.lean:16 (same declaration text).

4. def OAI.QuadricCounterexample.affineP1 line 16

   Also declared: ComparatorChallenges/QuadricBundles.lean:19 (same declaration text).

5. def OAI.QuadricCounterexample.affineQuadric line 19

   Also declared: ComparatorChallenges/QuadricBundles.lean:22 (same declaration text).

6. def OAI.QuadricCounterexample.coordP1 line 22

   Also declared: ComparatorChallenges/QuadricBundles.lean:25 (same declaration text).

7. def OAI.QuadricCounterexample.coordQuadric line 24

   Also declared: ComparatorChallenges/QuadricBundles.lean:27 (same declaration text).

8. def OAI.QuadricCounterexample.powerP1 line 27

   Also declared: ComparatorChallenges/QuadricBundles.lean:30 (same declaration text).

9. def OAI.QuadricCounterexample.powerQuadric line 29

   Also declared: ComparatorChallenges/QuadricBundles.lean:32 (same declaration text).

10. abbrev OAI.QuadricCounterexample.BaseCoordinates line 32

    Also declared: ComparatorChallenges/QuadricBundles.lean:35 (same declaration text).

11. abbrev OAI.QuadricCounterexample.FiberCoordinates line 33

    Also declared: ComparatorChallenges/QuadricBundles.lean:36 (same declaration text).

12. abbrev OAI.QuadricCounterexample.TwoMatrix line 34

    Also declared: ComparatorChallenges/QuadricBundles.lean:37 (same declaration text).

13. abbrev OAI.QuadricCounterexample.BasePolynomial line 35

    Also declared: ComparatorChallenges/QuadricBundles.lean:38 (same declaration text).

14. def OAI.QuadricCounterexample.baseEval line 36

    Also declared: ComparatorChallenges/QuadricBundles.lean:39 (same declaration text).

15. def OAI.QuadricCounterexample.AlgebraicallyRegularOn line 39

    Also declared: ComparatorChallenges/QuadricBundles.lean:42 (same declaration text).

16. def OAI.QuadricCounterexample.principalChart line 43

    Also declared: ComparatorChallenges/QuadricBundles.lean:46 (same declaration text).

17. structure OAI.QuadricCounterexample.AlgebraicRankTwoBundle line 46

    Also declared: ComparatorChallenges/QuadricBundles.lean:49 (same declaration text).

18. def OAI.QuadricCounterexample.AlgebraicRankTwoBundle.domain line 66

    Also declared: ComparatorChallenges/QuadricBundles.lean:70 (same declaration text).

19. def OAI.QuadricCounterexample.AlgebraicRankTwoBundle.coordinateDomain line 68

    Also declared: ComparatorChallenges/QuadricBundles.lean:72 (same declaration text).

20. def OAI.QuadricCounterexample.AlgebraicRankTwoBundle.dualTransition line 71

    Also declared: ComparatorChallenges/QuadricBundles.lean:75 (same declaration text).

21. def OAI.QuadricCounterexample.hyperplaneTransition line 75

    Also declared: ComparatorChallenges/QuadricBundles.lean:80 (same declaration text).

22. def OAI.QuadricCounterexample.polarizationTransition line 77

    Also declared: ComparatorChallenges/QuadricBundles.lean:82 (same declaration text).

23. def OAI.QuadricCounterexample.IsPowerPullbackTwist line 80

    Also declared: ComparatorChallenges/QuadricBundles.lean:85 (same declaration text).

24. structure OAI.QuadricCounterexample.SymmetricSection line 88

    Also declared: ComparatorChallenges/QuadricBundles.lean:93 (same declaration text).

25. def OAI.QuadricCounterexample.SymmetricSection.value line 97

    Also declared: ComparatorChallenges/QuadricBundles.lean:102 (same declaration text).

26. def OAI.QuadricCounterexample.ProjectiveAlgebraicCone line 101

    Also declared: ComparatorChallenges/QuadricBundles.lean:106 (same declaration text).

27. def OAI.QuadricCounterexample.sectionVector line 106

    Also declared: ComparatorChallenges/QuadricBundles.lean:111 (same declaration text).

28. def OAI.QuadricCounterexample.GivesClosedProjectiveEmbedding line 110

    Also declared: ComparatorChallenges/QuadricBundles.lean:115 (same declaration text).

29. def OAI.QuadricCounterexample.IsAmple line 133

    Also declared: ComparatorChallenges/QuadricBundles.lean:138 (same declaration text).

30. def OAI.QuadricCounterexample.holomorphicMetricDerivative line 137

    Also declared: ComparatorChallenges/QuadricBundles.lean:142 (same declaration text).

31. def OAI.QuadricCounterexample.metricMixedHessian line 141

    Also declared: ComparatorChallenges/QuadricBundles.lean:146 (same declaration text).

32. structure OAI.QuadricCounterexample.SmoothHermitianMetric line 146

    Also declared: ComparatorChallenges/QuadricBundles.lean:151 (same declaration text).

33. def OAI.QuadricCounterexample.SmoothHermitianMetric.StrictlyGriffithsPositive line 155

    Also declared: ComparatorChallenges/QuadricBundles.lean:160 (same declaration text).

34. def OAI.QuadricCounterexample.SourceMainTheorem line 162

    Also declared: ComparatorChallenges/QuadricBundles.lean:167 (same declaration text).