All.lean
Nyll.SchemeTheory.Modules.All
0 declarations indexed from sourceView source ↗
Module documentation
Canonical aggregate for SchemeTheory.Modules.
Imports114
- Nyll.SchemeTheory.Modules.ProjectivePresentationFaithfullyFlatDescent
- Nyll.SchemeTheory.Modules.FlatSectionsBaseChange
- Nyll.SchemeTheory.Modules.AffineFlatSectionsBaseChange
- Nyll.SchemeTheory.Modules.SectionsGluing
- Nyll.SchemeTheory.Modules.SpanningFrameDescent
- Nyll.SchemeTheory.Modules.SectionsLocalizationFiniteCover
- Nyll.SchemeTheory.Modules.SectionsAlgebra
- Nyll.SchemeTheory.Modules.PullbackUnitComposition
- Nyll.SchemeTheory.Modules.PullbackLocalSection
- Nyll.SchemeTheory.Modules.PullbackFrame
- Nyll.SchemeTheory.Modules.ProjectivePresentationIso
- Nyll.SchemeTheory.Modules.ProjectivePresentationFromFrames
- Nyll.SchemeTheory.Modules.ProjectivePresentationBaseChange
- Nyll.SchemeTheory.Modules.ProjectivePresentation
- Nyll.SchemeTheory.Modules.OpenImmersionUnit
- Nyll.SchemeTheory.Modules.LocallyTrivialSectionsLocalization
- Nyll.SchemeTheory.Modules.Invertible
- Nyll.SchemeTheory.Modules.Frames
- Nyll.SchemeTheory.Modules.FrameLocality
- Nyll.SchemeTheory.Modules.FrameLinearCombination
- Nyll.SchemeTheory.Modules.FrameFromTrivialization
- Nyll.SchemeTheory.Modules.FrameDescent
- Nyll.SchemeTheory.Modules.AffineSectionsBaseChange
- Nyll.SchemeTheory.Modules.PresheafPullbackMonoidal
- Nyll.SchemeTheory.Modules.Monoidal
- Nyll.SchemeTheory.Modules.InternalHomSheaf
- Nyll.SchemeTheory.Modules.SheafificationMonoidal
- Nyll.SchemeTheory.Modules.PresheafInternalHom
- Nyll.SchemeTheory.Modules.TensorSections
- Nyll.SchemeTheory.Modules.PullbackMonoidal
- Nyll.SchemeTheory.Modules.TensorPowers
- Nyll.SchemeTheory.Modules.TensorPowerComparison
- Nyll.SchemeTheory.Modules.AbelianSectionLocalization
- Nyll.SchemeTheory.Modules.QuasicoherentAffineLocalization
- Nyll.SchemeTheory.Modules.NativeSectionRestriction
- Nyll.SchemeTheory.Modules.LocalizationCriteria
- Nyll.SchemeTheory.Modules.SectionLocalization
- Nyll.SchemeTheory.Modules.PushforwardCoefficients
- Nyll.SchemeTheory.Modules.LocalizationRestrictionOfScalars
- Nyll.SchemeTheory.Modules.GlobalSectionLocalization
- Nyll.SchemeTheory.Modules.NativeSectionObjects
- Nyll.SchemeTheory.Modules.PushforwardSectionComparison
- Nyll.SchemeTheory.Modules.PushforwardLocalization
- Nyll.SchemeTheory.Modules.FiniteRelativeSpec
- Nyll.SchemeTheory.Modules.GeneratedAlgebraPresheaf
- Nyll.SchemeTheory.Modules.GeneratedAlgebraLocalization
- Nyll.SchemeTheory.Modules.GeneratedFiniteAlgebra
- Nyll.SchemeTheory.Modules.AffineSourceColimit
- Nyll.SchemeTheory.Modules.DirectImageAlgebra
- Nyll.SchemeTheory.Modules.GeneratedAlgebraSource
- Nyll.SchemeTheory.Modules.QuasicoherentLocal
- Nyll.SchemeTheory.Modules.QuasicoherentKernel
- Nyll.SchemeTheory.Modules.QuasicoherentKernelGlobal
- Nyll.SchemeTheory.Modules.PushforwardRestrict
- Nyll.SchemeTheory.Modules.QuasicoherentPushforward
- Nyll.SchemeTheory.Modules.DirectImageAlgebraQuasicoherent
- Nyll.SchemeTheory.Modules.QuasicoherentCokernel
- Nyll.SchemeTheory.Modules.KernelSubmodule
- Nyll.SchemeTheory.Modules.QuasicoherentExtension
- Nyll.SchemeTheory.Modules.SubmoduleEmbeddedIso
- Nyll.SchemeTheory.Modules.KernelSubmoduleScheme
- Nyll.SchemeTheory.Modules.SubmoduleGluing
- Nyll.SchemeTheory.Modules.GeneratedAlgebraLocalFactors
- Nyll.SchemeTheory.Modules.SubmoduleGluingQuasicoherent
- Nyll.SchemeTheory.Modules.FiniteTypeTilde
- Nyll.SchemeTheory.Modules.FiniteTypeLocality
- Nyll.SchemeTheory.Modules.FiniteTypeQuotient
- Nyll.SchemeTheory.Modules.ImageSubmodule
- Nyll.SchemeTheory.Modules.QuasicoherentImage
- Nyll.SchemeTheory.Modules.QuasicoherentCoprod
- Nyll.SchemeTheory.Modules.FiniteTypeCoprod
- Nyll.SchemeTheory.Modules.AffineFiniteSubmodule
- Nyll.SchemeTheory.Modules.ImageSubmoduleRestriction
- Nyll.SchemeTheory.Modules.FiniteQuasicoherentSum
- Nyll.SchemeTheory.Modules.FiniteTypeRestriction
- Nyll.SchemeTheory.Modules.SubmoduleGluingFiniteType
- Nyll.SchemeTheory.Modules.QuasicoherentSubmoduleOverExtension
- Nyll.SchemeTheory.Modules.FiniteGeneratingSections
- Nyll.SchemeTheory.Modules.AffineSubmoduleLocalization
- Nyll.SchemeTheory.Modules.FiniteTypePushforward
- Nyll.SchemeTheory.Modules.FiniteTypeSchemeRestriction
- Nyll.SchemeTheory.Modules.FiniteTypeTop
- Nyll.SchemeTheory.Modules.AffineFiniteSubmoduleExtension
- Nyll.SchemeTheory.Modules.AffineModuleEpi
- Nyll.SchemeTheory.Modules.AffineOpenModuleEpi
- Nyll.SchemeTheory.Modules.FiniteTypeAffineSections
- Nyll.SchemeTheory.Modules.SubmoduleCoverEquality
- Nyll.SchemeTheory.Modules.SubmoduleOverEquality
- Nyll.SchemeTheory.Modules.SubmoduleRestrictionComparison
- Nyll.SchemeTheory.Modules.AffineSectionLocalizationFinite
- Nyll.SchemeTheory.Modules.FiniteTypeLocalAffineSections
- Nyll.SchemeTheory.Modules.FiniteSectionSubmodule
- Nyll.SchemeTheory.Modules.SubmoduleTopRestriction
- Nyll.SchemeTheory.Modules.KernelSubmoduleRestriction
- Nyll.SchemeTheory.Modules.FiniteOpenSectionSubmodule
- Nyll.SchemeTheory.Modules.SubmoduleRestrictedSections
- Nyll.SchemeTheory.Modules.FiniteTypeIteratedSlice
- Nyll.SchemeTheory.Modules.FiniteTypeSubopen
- Nyll.SchemeTheory.Modules.SubmoduleGluingUnion
- Nyll.SchemeTheory.Modules.FiniteSubmoduleUnionExtension
- Nyll.SchemeTheory.Modules.AffineFiniteSubmoduleOnOpen
- Nyll.SchemeTheory.Modules.AffineChartFiniteSubmoduleExtension
- Nyll.SchemeTheory.Modules.FiniteSubmoduleExtension
- Nyll.SchemeTheory.Modules.FiniteLocalSectionExtension
- Nyll.SchemeTheory.Modules.FiniteAffineSectionSubmodule
- Nyll.SchemeTheory.Modules.TensorFrames
- Nyll.SchemeTheory.Modules.TensorPowerFrames
- Nyll.SchemeTheory.Modules.TensorSectionMaps
- Nyll.SchemeTheory.Modules.TensorSectionRightUnitor
- Nyll.SchemeTheory.Modules.TensorSectionSheafification
- Nyll.SchemeTheory.Modules.TensorSectionAssociator
- Nyll.SchemeTheory.Modules.TensorPowerSectionProduct
- Nyll.SchemeTheory.Modules.SectionRing
- Nyll.SchemeTheory.Modules.SectionRingConstruction
Imported by1
This module has no indexed declarations. Its imports and full source are available here.