All.lean
Nyll.SchemeTheory.Affine.All
0 declarations indexed from sourceView source ↗
Module documentation
Affine scheme infrastructure
This facade collects affine-over-base colimits, affine morphism properties, flat minimal-prime control, and geometric irreducibility of affine schemes.
Imports22
- Nyll.SchemeTheory.Affine.SeparatedIntersections
- Nyll.SchemeTheory.Affine.PullbackSectionsPushout
- Nyll.SchemeTheory.Affine.FlatBaseChangeSections
- Nyll.SchemeTheory.Affine.FlatMinimalPrime
- Nyll.SchemeTheory.Affine.GeometricPointLocalization
- Nyll.SchemeTheory.Affine.RegularSection
- Nyll.SchemeTheory.Affine.StalkLocalization
- Nyll.SchemeTheory.Affine.WeilRestriction.All
- Nyll.SchemeTheory.Affine.PrimePairHartogs
- Nyll.SchemeTheory.Affine.RegularPairHartogs
- Nyll.SchemeTheory.Affine.FlatBaseChangeAffinization
- Nyll.SchemeTheory.Affine.AffinizationDescent
- Nyll.SchemeTheory.Affine.ChartStalkLocalization
- Nyll.SchemeTheory.Affine.StalkBaseChange
- Nyll.SchemeTheory.Affine.SpecSectionMap
- Nyll.SchemeTheory.Affine.HomeomorphismIdempotentSections
- Nyll.SchemeTheory.Affine.ConnectedOfGlobalSections
- Nyll.SchemeTheory.Affine.GeometricallyConnectedOfGlobalSections
- Nyll.SchemeTheory.Affine.FaithfullyFlatSectionSurjectivity
- Nyll.SchemeTheory.Affine.SpecFlatBaseChangeSections
- Nyll.SchemeTheory.Affine.SurjectiveSectionPushout
- Nyll.SchemeTheory.Affine.StalkBaseChangeSections
Imported by1
This module has no indexed declarations. Its imports and full source are available here.