All.lean
Nyll.SchemeTheory.Morphisms.All
0 declarations indexed from sourceView source ↗
Module documentation
Scheme morphisms
This facade collects the finite, flat, smooth, rank, reduced-etale, and closed-immersion lemmas used by the finite étale and fundamental-group developments.
Imports36
- Nyll.SchemeTheory.Morphisms.ClosedImmersionLift
- Nyll.SchemeTheory.Morphisms.DominantBaseChange
- Nyll.SchemeTheory.Morphisms.EtaleRadicial
- Nyll.SchemeTheory.Morphisms.EtaleReduced
- Nyll.SchemeTheory.Morphisms.FiniteDescent
- Nyll.SchemeTheory.Morphisms.GeometricallyIntegralDescent
- Nyll.SchemeTheory.Morphisms.NormalizationFiniteFactor
- Nyll.SchemeTheory.Morphisms.OpenImmersionLocalization
- Nyll.SchemeTheory.Morphisms.OpenImmersionQuotient
- Nyll.SchemeTheory.Morphisms.RadicialDescent
- Nyll.SchemeTheory.Morphisms.SigmaPullback
- Nyll.SchemeTheory.Morphisms.UnramifiedHomExt
- Nyll.SchemeTheory.Morphisms.SmoothGeometricallyIntegral
- Nyll.SchemeTheory.Morphisms.GeometricallyIrreducibleOverAlgebraicallyClosed
- Nyll.SchemeTheory.Morphisms.GeometricallyIrreducibleConnected
- Nyll.SchemeTheory.Morphisms.GeometricallyIntegralFieldDescent
- Nyll.SchemeTheory.Morphisms.FiberRank
- Nyll.SchemeTheory.Morphisms.QuasiFinite
- Nyll.SchemeTheory.Morphisms.UnramifiedPointRigidity
- Nyll.SchemeTheory.Morphisms.ResiduePointFixedness
- Nyll.SchemeTheory.Morphisms.ProperNormalization
- Nyll.SchemeTheory.Morphisms.FlatBaseChangeNormalization
- Nyll.SchemeTheory.Morphisms.AffineNormalizationPushforward
- Nyll.SchemeTheory.Morphisms.NormalizationPushforward
- Nyll.SchemeTheory.Morphisms.NormalizationFlatBaseChangeIso
- Nyll.SchemeTheory.Morphisms.EtalePostcomposition
- Nyll.SchemeTheory.Morphisms.FiniteEtaleGeometricallyReduced
- Nyll.SchemeTheory.Morphisms.ProperHenselianClosedRestriction
- Nyll.SchemeTheory.Morphisms.ProperHenselianClopenLift
- Nyll.SchemeTheory.Morphisms.ProperIntegralHenselianConnectedFiber
- Nyll.SchemeTheory.Morphisms.ProperIntegralHenselianSections
- Nyll.SchemeTheory.Morphisms.NoetherianProperFiberSections
- Nyll.SchemeTheory.Morphisms.ChowDatumProj_nonempty_of
- Nyll.SchemeTheory.Morphisms.ChowDatum_nonempty
- Nyll.SchemeTheory.Morphisms.exists_appTop_pullback_map_eq_appTop_pullback_fst_of_isProper
- Nyll.SchemeTheory.Morphisms.ProperHenselianSheafRestriction
Imported by1
This module has no indexed declarations. Its imports and full source are available here.