OAI/NumberTheory/PiExponent/Ampleness/
768 declarations, 0 contain sorry, 0 declared as axioms; 119 files
Files
- AdmissibleBlowupAmple.lean 1 declarations
- AdmissibleBlowupGeometry.lean 49 declarations
- AdmissibleBlowupMargin.lean 3 declarations
- AdmissibleBlowupPolarization.lean 9 declarations
- AdmissibleCurveModelDegrees.lean 1 declarations
- AdmissibleJetAmpleness.lean 1 declarations
- AffineBlowupUniversal.lean 4 declarations
- AffineFunctionFieldCompatibility.lean 5 declarations
- AffineReesCanonicalRecovery.lean 1 declarations
- AmpleAllPowersGeneration.lean 2 declarations
- AmpleCommonDegree.lean 2 declarations
- AmpleCurveDegreePositive.lean 7 declarations
- AmpleDivisorDimension.lean 3 declarations
- AmpleDivisorDimensionBase.lean 4 declarations
- AmpleFiniteProjectiveEmbedding.lean 1 declarations
- AmpleFromCover.lean 2 declarations
- AmpleGeneratedTensor.lean 7 declarations
- AmpleGlobalGeneration.lean 7 declarations
- AmpleIso.lean 3 declarations
- AmplePositiveTwist.lean 2 declarations
- AmpleProjectiveSections.lean 5 declarations
- AmpleSlopeAlgebra.lean 11 declarations
- AmpleSlopeTopology.lean 9 declarations
- AmpleThresholdPolynomial.lean 5 declarations
- BlowupAffineSections.lean 1 declarations
- BlowupAmpleTwist.lean 3 declarations
- BlowupComplement.lean 4 declarations
- BlowupCurveMargin.lean 13 declarations
- BlowupIdeal.lean 24 declarations
- BlowupJetReesReduction.lean 1 declarations
- BlowupJetSurjectivity.lean 5 declarations
- BlowupJetSurjectivityComplete.lean 1 declarations
- BlowupPresentationRestriction.lean 2 declarations
- BlowupProperIntegral.lean 27 declarations
- BlowupSchemeExt.lean 12 declarations
- BlowupUniversalBaseChange.lean 8 declarations
- ClosedAmpleBaseChange.lean 5 declarations
- ClosedAmpleRestriction.lean 4 declarations
- CoherentAffineFinite.lean 17 declarations
- ComponentAmpleDescent.lean 3 declarations
- ComponentAmpleDescentCover.lean 4 declarations
- ComponentAmpleDescentIdeal.lean 3 declarations
- ComponentAmpleDescentLocal.lean 1 declarations
- ComponentAmpleDescentSupported.lean 1 declarations
- CurveBlowupImage.lean 11 declarations
- CurveBlowupImageBase.lean 6 declarations
- CurveNormalizationPolarization.lean 6 declarations
- ExceptionalAffineChart.lean 10 declarations
- ExceptionalAffineChartRestriction.lean 13 declarations
- ExceptionalChartPullbackValue.lean 2 declarations
- ExceptionalCurveDegree.lean 22 declarations
- ExceptionalPowerPresentation.lean 4 declarations
- ExceptionalPowerSections.lean 7 declarations
- ExceptionalRecoveryMap.lean 4 declarations
- ExceptionalRecoveryTwist.lean 1 declarations
- ExceptionalRepresentedOpaque.lean 5 declarations
- ExceptionalRepresentedTypes.lean 5 declarations
- ExceptionalRepresentedValue.lean 1 declarations
- ExceptionalTypedRestriction.lean 3 declarations
- ExceptionalTypedTransport.lean 4 declarations
- ExceptionalTypedTransportNaturality.lean 1 declarations
- FiniteAffineFrames.lean 1 declarations
- FinitePullbackAmple.lean 2 declarations
- FiniteReesComparison.lean 3 declarations
- GlobalBlowupAffineSquare.lean 8 declarations
- GlobalBlowupGluing.lean 31 declarations
- GlobalBlowupJetSurjectivity.lean 2 declarations
- GlobalBlowupRestriction.lean 7 declarations
- GlobalExceptionalComparison.lean 13 declarations
- GlobalReesCanonicalRecovery.lean 1 declarations
- GlobalReesRecoveryComparison.lean 4 declarations
- IntegralComponentAmple.lean 1 declarations
- LineAmpleOperations.lean 3 declarations
- LocalHomogeneousDegrees.lean 1 declarations
- NakaiAmpleFromSections.lean 2 declarations
- NakaiBasepointFree.lean 3 declarations
- NakaiCartier.lean 9 declarations
- NakaiDivisorAmple.lean 3 declarations
- NakaiEffectivity.lean 2 declarations
- NakaiInductionStep.lean 3 declarations
- NakaiSectionLifting.lean 2 declarations
- NakaiStationarity.lean 3 declarations
- NefAmple.lean 11 declarations
- NilpotentAmpleDescent.lean 3 declarations
- NoetherianAmpleProjectiveSections.lean 2 declarations
- NumericalAmpleness.lean 6 declarations
- NumericalAmplenessTheorem.lean 2 declarations
- ProjectiveO1Ample.lean 1 declarations
- ProperAmpleFiniteDimension.lean 6 declarations
- ReducedComponentAmple.lean 2 declarations
- ReesExceptional.lean 16 declarations
- ReesExceptionalSheaf.lean 1 declarations
- ReesFiniteCover.lean 5 declarations
- ReesFixedChart.lean 13 declarations
- ReesFixedFrames.lean 3 declarations
- ReesFixedPower.lean 8 declarations
- ReesFixedPowerRestriction.lean 1 declarations
- ReesFixedRestriction.lean 3 declarations
- ReesGradedModule.lean 9 declarations
- ReesLocalizedChart.lean 11 declarations
- ReesLocalizedIntersections.lean 13 declarations
- ReesPolynomialPresentation.lean 10 declarations
- ReesPrincipalLift.lean 16 declarations
- ReesProductAugmentation.lean 4 declarations
- ReesProductChart.lean 17 declarations
- ReesProductFrames.lean 2 declarations
- ReesProductPower.lean 5 declarations
- ReesProductRestriction.lean 10 declarations
- ReesProductSchemeChart.lean 10 declarations
- ReesProductSchemeRestriction.lean 1 declarations
- ReesPushdown.lean 47 declarations
- ReesRelativeSections.lean 6 declarations
- ReesSectionInclusion.lean 5 declarations
- ReesSheafCanonicalValue.lean 3 declarations
- ReesUniversalUniqueness.lean 17 declarations
- RelativeAffineSectionAmple.lean 1 declarations
- WeightedAffineFrame.lean 3 declarations
- WeightedProjectiveAmple.lean 1 declarations
- ZeroDimensionalAmple.lean 2 declarations