All.lean
Nyll.SchemeTheory.Descent.All
0 declarations indexed from sourceView source ↗
Imports39
- Nyll.SchemeTheory.Descent.AffineAlgebraCoaction
- Nyll.SchemeTheory.Descent.AffineCocycle
- Nyll.SchemeTheory.Descent.AffineIntegralLimit
- Nyll.SchemeTheory.Descent.AffineActionCoordinates
- Nyll.SchemeTheory.Descent.ActionOverlap
- Nyll.SchemeTheory.Descent.AlgebraCoaction
- Nyll.SchemeTheory.Descent.FaithfullyFlatAlgebra
- Nyll.SchemeTheory.Descent.Equivariance
- Nyll.SchemeTheory.Descent.EffectiveAffine
- Nyll.SchemeTheory.Descent.FpqcLocalCoequalizer
- Nyll.SchemeTheory.Descent.AffineTransitionHom
- Nyll.SchemeTheory.Descent.AffineTransitionEquality
- Nyll.SchemeTheory.Descent.AffineTransitionOverEquality
- Nyll.SchemeTheory.Descent.AffineTransitionHomFamily
- Nyll.SchemeTheory.Descent.AffineTransitionOverComparison
- Nyll.SchemeTheory.Descent.AffineTransitionOverHomFamily
- Nyll.SchemeTheory.Descent.AffineChartCompatibleStalkSpreading
- Nyll.SchemeTheory.Descent.AlgebraCoactionTransport
- Nyll.SchemeTheory.Descent.CanonicalAlgebraEqualizer
- Nyll.SchemeTheory.Descent.CompatibleStalkSpreading
- Nyll.SchemeTheory.Descent.InvariantScalarExtensionComparison
- Nyll.SchemeTheory.Descent.RadicialModelCoaction
- Nyll.SchemeTheory.Descent.StalkSpreading
- Nyll.SchemeTheory.Descent.RetrocompactStalkSpreading
- Nyll.SchemeTheory.Descent.RetrocompactAffineChartStalkSpreading
- Nyll.SchemeTheory.Descent.PunctureSectionSpreading
- Nyll.SchemeTheory.Descent.PunctureIsoSpreading
- Nyll.SchemeTheory.Descent.StalkSpreadingOpen
- Nyll.SchemeTheory.Descent.AffineTransitionIdempotents
- Nyll.SchemeTheory.Descent.AffineTransitionImageDiagram
- Nyll.SchemeTheory.Descent.AffineTransitionImageLimit
- Nyll.SchemeTheory.Descent.NoetherianImageApproximation
- Nyll.SchemeTheory.Descent.NoetherianImageResidueLimit
- Nyll.SchemeTheory.Descent.LocalStageResidueComparison
- Nyll.SchemeTheory.Descent.NoetherianImageIdempotentLift
- Nyll.SchemeTheory.Descent.FGSubalgebra
- Nyll.SchemeTheory.Descent.SubalgebraStages
- Nyll.SchemeTheory.Descent.SubalgebraStages_nonempty_isLimit_cone
- Nyll.SchemeTheory.Descent.EqualizerScalars
Imported by1
This module has no indexed declarations. Its imports and full source are available here.