All.lean
Nyll.SchemeTheory.FiniteEtale.All
0 declarations indexed from sourceView source ↗
Module documentation
Finite étale scheme theory
This facade collects affine Weil restriction, fpqc descent for finite étale algebras, exactness of the forgetful functor, and étale schemes over a field.
Imports57
- Nyll.SchemeTheory.FiniteEtale.AffineEquivalence
- Nyll.SchemeTheory.FiniteEtale.AffineThickening
- Nyll.SchemeTheory.FiniteEtale.AffineUniversalHomeomorphismModel
- Nyll.SchemeTheory.FiniteEtale.Algebra.All
- Nyll.SchemeTheory.FiniteEtale.Away.All
- Nyll.SchemeTheory.FiniteEtale.BaseChange.All
- Nyll.SchemeTheory.FiniteEtale.ClopenFull
- Nyll.SchemeTheory.FiniteEtale.ClopenPullback
- Nyll.SchemeTheory.FiniteEtale.ConnectedFiberSections
- Nyll.SchemeTheory.FiniteEtale.ConnectedFiberFullyFaithful
- Nyll.SchemeTheory.FiniteEtale.MaximalOpenExtension
- Nyll.SchemeTheory.FiniteEtale.FullOfSectionDescent
- Nyll.SchemeTheory.FiniteEtale.DensePullback
- Nyll.SchemeTheory.FiniteEtale.DVRUnramifiedExtension
- Nyll.SchemeTheory.FiniteEtale.Forget.All
- Nyll.SchemeTheory.FiniteEtale.Henselian.All
- Nyll.SchemeTheory.FiniteEtale.Local.All
- Nyll.SchemeTheory.FiniteEtale.LocalSplitting
- Nyll.SchemeTheory.FiniteEtale.PullbackFaithful
- Nyll.SchemeTheory.FiniteEtale.PullbackRepresentable
- Nyll.SchemeTheory.FiniteEtale.RadicialDescentCocycle
- Nyll.SchemeTheory.FiniteEtale.RadicialDescentIso
- Nyll.SchemeTheory.FiniteEtale.RingCover
- Nyll.SchemeTheory.FiniteEtale.ThickeningFullyFaithful
- Nyll.SchemeTheory.FiniteEtale.ThickeningGluing
- Nyll.SchemeTheory.FiniteEtale.UniversalHomeomorphismFullyFaithful
- Nyll.SchemeTheory.FiniteEtale.SectionsDescent
- Nyll.SchemeTheory.FiniteEtale.AffinizationExtension
- Nyll.SchemeTheory.FiniteEtale.PointSections
- Nyll.SchemeTheory.FiniteEtale.InverseLimitHom
- Nyll.SchemeTheory.FiniteEtale.InverseLimitEquality
- Nyll.SchemeTheory.FiniteEtale.FilteredColimitSpec
- Nyll.SchemeTheory.FiniteEtale.AffineTransitionModel
- Nyll.SchemeTheory.FiniteEtale.AffineTransitionCharts
- Nyll.SchemeTheory.FiniteEtale.RelativeGluing
- Nyll.SchemeTheory.FiniteEtale.TwoOpenGluing
- Nyll.SchemeTheory.FiniteEtale.InverseLimitIsomorphism
- Nyll.SchemeTheory.FiniteEtale.AffineTransitionLocalModel
- Nyll.SchemeTheory.FiniteEtale.InverseLimitOpenEquations
- Nyll.SchemeTheory.FiniteEtale.InverseLimitFiniteCover
- Nyll.SchemeTheory.FiniteEtale.InverseLimitIsoDescent
- Nyll.SchemeTheory.FiniteEtale.InverseLimitIsoModels
- Nyll.SchemeTheory.FiniteEtale.InverseLimitOpenIsomorphisms
- Nyll.SchemeTheory.FiniteEtale.AffineTransitionOverlapRecovery
- Nyll.SchemeTheory.FiniteEtale.InverseLimitGluingRelations
- Nyll.SchemeTheory.FiniteEtale.RelativePullbackGluing
- Nyll.SchemeTheory.FiniteEtale.RelativeOverlapFiniteness
- Nyll.SchemeTheory.FiniteEtale.InverseLimitRecoveredModel
- Nyll.SchemeTheory.FiniteEtale.RawOverlapFiniteness
- Nyll.SchemeTheory.FiniteEtale.InverseLimitRawCharts
- Nyll.SchemeTheory.FiniteEtale.InverseLimitRawModel
- Nyll.SchemeTheory.FiniteEtale.InverseLimitModel
- Nyll.SchemeTheory.FiniteEtale.StrictLocalSections
- Nyll.SchemeTheory.FiniteEtale.ProperClosedFiberFaithful
- Nyll.SchemeTheory.FiniteEtale.ProperHenselianSections
- Nyll.SchemeTheory.FiniteEtale.AffineUniversalHomeomorphismEquivalence
- Nyll.SchemeTheory.FiniteEtale.isIso_of_isIso_pullback_closedFibre_of_isFinite_of_etale_of_isProper
Imported by1
This module has no indexed declarations. Its imports and full source are available here.