OAI/AlgebraicGeometry/StableCoordinate/
1570 declarations, 0 contain sorry, 0 declared as axioms; 118 files
Files
- ActionWeightDerivative.lean 8 declarations
- AffineGeometry.lean 20 declarations
- AffineNormalization.lean 8 declarations
- All.lean 0 declarations
- AllFibers.lean 3 declarations
- AmbientMaps.lean 14 declarations
- AssociatedGradedPresentation.lean 12 declarations
- BundleCharts.lean 40 declarations
- BundlePrincipalization.lean 12 declarations
- ChartIntersection.lean 7 declarations
- ChartLNDConstant.lean 2 declarations
- CoactionAction.lean 10 declarations
- CoactionBaseNaturality.lean 2 declarations
- CoactionLND.lean 14 declarations
- CoordinateDerivation.lean 16 declarations
- CoordinateLeadingDerivation.lean 8 declarations
- CoordinateToQuadric.lean 2 declarations
- Definitions.lean 13 declarations
- Degree.lean 5 declarations
- DerivationScalarUpgrade.lean 7 declarations
- DerivationTopShift.lean 5 declarations
- DeterminantActionWeights.lean 5 declarations
- DeterminantCharts.lean 74 declarations
- DeterminantDomain.lean 10 declarations
- DeterminantFinalStep.lean 1 declarations
- DeterminantGradedObstruction.lean 4 declarations
- DeterminantGradings.lean 26 declarations
- DeterminantIntersection.lean 2 declarations
- DeterminantLeadingReduction.lean 1 declarations
- DeterminantLiftWeights.lean 11 declarations
- DeterminantNonzero.lean 18 declarations
- DeterminantPrimeA.lean 29 declarations
- DeterminantRigidity.lean 17 declarations
- DeterminantRing.lean 29 declarations
- DeterminantUFD.lean 4 declarations
- DeterminantWeights.lean 20 declarations
- ExponentialShift.lean 31 declarations
- FactorialClosure.lean 7 declarations
- FilteredRees.lean 15 declarations
- FilteredReesDerivation.lean 25 declarations
- FiltrationDerivationShift.lean 13 declarations
- FiltrationSeparation.lean 26 declarations
- FrameCoassociativity.lean 8 declarations
- FrameLiftCoassoc.lean 8 declarations
- FrameLiftUniqueness.lean 17 declarations
- FrameNormalization.lean 13 declarations
- FrameQuotientMap.lean 27 declarations
- FrameScaling.lean 8 declarations
- GeometricInterpretation.lean 12 declarations
- GradedDegeneration.lean 25 declarations
- GradedPresentationKernel.lean 4 declarations
- GradedPresentationMap.lean 23 declarations
- GradedRelation.lean 9 declarations
- GradedRelationSanity.lean 9 declarations
- HomogeneousQuotient.lean 16 declarations
- HomogeneousQuotientWeight.lean 19 declarations
- IntegerFiltrationDegree.lean 13 declarations
- IteratedQuotient.lean 10 declarations
- LNDAction.lean 11 declarations
- LNDExponential.lean 16 declarations
- LNDExponentialLaw.lean 9 declarations
- LaurentDerivationTransport.lean 10 declarations
- LaurentLNDDescent.lean 15 declarations
- LaurentPresentation.lean 48 declarations
- LaurentWeightObstruction.lean 8 declarations
- LaurentWeightedMap.lean 6 declarations
- LeadingComponent.lean 35 declarations
- LeadingLocallyNilpotent.lean 3 declarations
- LiftObstruction.lean 7 declarations
- Linearization.lean 41 declarations
- LocalizationIntersection.lean 7 declarations
- LocalizationLND.lean 26 declarations
- MatrixChange.lean 23 declarations
- ModificationEmbedding.lean 18 declarations
- ModificationPieces.lean 32 declarations
- NonCoordinate.lean 1 declarations
- NonnegativeWeights.lean 8 declarations
- NonzeroFiber.lean 45 declarations
- NonzeroFiberAssembly.lean 2 declarations
- NonzeroFiberTransport.lean 4 declarations
- NormalizedDeterminantLift.lean 22 declarations
- ObstructionDefinitions.lean 30 declarations
- ObstructionDomains.lean 13 declarations
- ObstructionPrincipalization.lean 13 declarations
- PicardUFD.lean 5 declarations
- PolynomialChartIntersection.lean 6 declarations
- PolynomialFrameNormalization.lean 9 declarations
- Presentation.lean 55 declarations
- Principal.lean 7 declarations
- PrincipalIdeal.lean 5 declarations
- PrincipalInitialRelation.lean 6 declarations
- QuadricFactorization.lean 7 declarations
- QuotientTransport.lean 6 declarations
- Rectifiability.lean 4 declarations
- ReesCoefficientCriterion.lean 3 declarations
- ReesCoefficientKernel.lean 3 declarations
- ReesToDegeneration.lean 13 declarations
- Rigidity.lean 2 declarations
- RigidityCoefficients.lean 8 declarations
- SourceCoordinateTransport.lean 2 declarations
- SourceFiltrationProper.lean 16 declarations
- SourceInvariant.lean 1 declarations
- SourceLocalizedDerivation.lean 8 declarations
- SourcePresentation.lean 5 declarations
- Stabilization.lean 16 declarations
- StabilizationEmbedding.lean 8 declarations
- StabilizedQuotient.lean 16 declarations
- UnitCocycle.lean 6 declarations
- UnivariateLND.lean 6 declarations
- VerticalLND.lean 8 declarations
- WeightedInitial.lean 18 declarations
- WeightedInitialIdeal.lean 8 declarations
- WeightedInitialKernel.lean 3 declarations
- ZeroFiber.lean 17 declarations
- ZeroFiberExact.lean 2 declarations
- ZeroFiberSpecialization.lean 28 declarations
- ZeroFiberTransport.lean 1 declarations
- ZeroLocusInterface.lean 12 declarations