OAI/AlgebraicGeometry/Seshadri/Sheaves/
368 declarations, 0 contain sorry, 0 declared as axioms; 51 files
Files
- AffineLocalizing.lean 12 declarations
- AffineOrderRestriction.lean 4 declarations
- AmpleFramedCover.lean 1 declarations
- BaseChangeNatural.lean 1 declarations
- CartierModule.lean 43 declarations
- CartierRestriction.lean 3 declarations
- CartierTensor.lean 12 declarations
- ChartModuleMap.lean 5 declarations
- ClosedModuleExact.lean 2 declarations
- ClosedPushforwardEuler.lean 7 declarations
- ClosedPushforwardExact.lean 5 declarations
- DiscreteLineBundle.lean 4 declarations
- EtaleLineFrame.lean 1 declarations
- FramedPullback.lean 4 declarations
- Frames.lean 25 declarations
- LineBundleCoherent.lean 10 declarations
- LinePullback.lean 3 declarations
- LinePullbackTensor.lean 4 declarations
- ModuleLocal.lean 6 declarations
- OpenBaseChange.lean 6 declarations
- OpenPullbackUnit.lean 2 declarations
- PlaneModules.lean 5 declarations
- PlaneProjectionModule.lean 6 declarations
- PowerExtension.lean 15 declarations
- PullbackSectionLinear.lean 2 declarations
- PullbackSectionOpenExact.lean 2 declarations
- PullbackTensorRestrict.lean 3 declarations
- PushforwardTensor.lean 7 declarations
- RestrictTensorMap.lean 3 declarations
- RestrictedGenerators.lean 2 declarations
- RestrictedSections.lean 3 declarations
- Restriction.lean 39 declarations
- RestrictionLocalization.lean 4 declarations
- SectionOpens.lean 16 declarations
- SectionPullback.lean 6 declarations
- Sections.lean 15 declarations
- SupportedSheaf.lean 4 declarations
- TensorAssocPure.lean 2 declarations
- TensorCurveEuler.lean 6 declarations
- TensorDivision.lean 11 declarations
- TensorFramePure.lean 2 declarations
- TensorFrames.lean 18 declarations
- TensorInclusion.lean 5 declarations
- TensorOpenSection.lean 4 declarations
- TensorOpenSquare.lean 4 declarations
- TensorPowerDistribution.lean 4 declarations
- TensorPowerPure.lean 2 declarations
- TensorPure.lean 10 declarations
- TensorRestrictPure.lean 3 declarations
- TensorSectionOpen.lean 2 declarations
- TensorUnitPure.lean 3 declarations