WeaklyEtale

📁 Source: Mathlib/AlgebraicGeometry/Morphisms/WeaklyEtale.lean

Statistics

Metric	Count
Definitions WeaklyEtale	1
Theorems flat, flat_diagonal, instCompScheme, instDiagonalScheme, instFstScheme, instHasOfPostcompPropertyScheme, instIsMultiplicativeScheme, instIsStableUnderBaseChangeScheme, instIsZariskiLocalAtSource, instIsZariskiLocalAtTarget, instMorphismRestrict, instOfEtale, instResLE, instRespectsIsoScheme, instSndScheme, of_comp, weaklyEtale_eq_flat_inf_diagonal_flat, etale_le_weaklyEtale, weaklyEtale_iff	19
Total	20

AlgebraicGeometry

Definitions

Name	Category	Theorems
WeaklyEtale 📖	CompData	26 math math: WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat, weaklyEtale_iff, Scheme.proetalePrecoverage_le_precoverage_weaklyEtale, WeaklyEtale.instFstScheme, WeaklyEtale.instIsStableUnderBaseChangeScheme, WeaklyEtale.instResLE, Scheme.ProEt.forget_obj, etale_le_weaklyEtale, WeaklyEtale.instCompScheme, WeaklyEtale.instMorphismRestrict, WeaklyEtale.instRespectsIsoScheme, WeaklyEtale.instIsZariskiLocalAtSource, WeaklyEtale.instOfEtale, Scheme.ProEt.forget_map, WeaklyEtale.instIsMultiplicativeScheme, Scheme.ProEt.mk_hom, WeaklyEtale.instHasOfPostcompPropertyScheme, WeaklyEtale.instSndScheme, Scheme.ProEt.instWeaklyEtaleHomDiscretePUnit, WeaklyEtale.of_comp, Scheme.proetaleTopology_eq_propQCTopology, Scheme.instWeaklyEtaleF, WeaklyEtale.instDiagonalScheme, WeaklyEtale.instIsZariskiLocalAtTarget, Scheme.ProEt.mk_right_as, Scheme.ProEt.mk_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
etale_le_weaklyEtale 📖	mathematical	—	Pi.hasLe Scheme Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Scheme.instCategory Prop.le Etale WeaklyEtale	—	WeaklyEtale.instOfEtale
weaklyEtale_iff 📖	mathematical	—	WeaklyEtale Flat CategoryTheory.Limits.pullback.diagonalObj Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.diagonal	—	Scheme.Pullback.instHasPullback

AlgebraicGeometry.WeaklyEtale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
flat 📖	mathematical	—	AlgebraicGeometry.Flat	—	—
flat_diagonal 📖	mathematical	—	AlgebraicGeometry.Flat CategoryTheory.Limits.pullback.diagonalObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.diagonal	—	—
instCompScheme 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory	—	CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeScheme
instDiagonalScheme 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale CategoryTheory.Limits.pullback.diagonalObj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.diagonal	—	AlgebraicGeometry.Scheme.Pullback.instHasPullback flat_diagonal flat instOfEtale AlgebraicGeometry.Etale.instOfIsOpenImmersion AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono AlgebraicGeometry.IsPreimmersion.instMonoScheme AlgebraicGeometry.IsImmersion.toIsPreimmersion AlgebraicGeometry.IsImmersion.instDiagonalScheme
instFstScheme 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeScheme
instHasOfPostcompPropertyScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.HasOfPostcompProperty AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.WeaklyEtale	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal instIsStableUnderBaseChangeScheme instIsMultiplicativeScheme instDiagonalScheme
instIsMultiplicativeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.WeaklyEtale	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks weaklyEtale_eq_flat_inf_diagonal_flat CategoryTheory.MorphismProperty.IsMultiplicative.inf AlgebraicGeometry.Flat.instIsMultiplicativeScheme CategoryTheory.MorphismProperty.instIsMultiplicativeDiagonalOfIsStableUnderBaseChange AlgebraicGeometry.Flat.isStableUnderBaseChange
instIsStableUnderBaseChangeScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.WeaklyEtale	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks weaklyEtale_eq_flat_inf_diagonal_flat CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf AlgebraicGeometry.Flat.isStableUnderBaseChange CategoryTheory.MorphismProperty.IsStableUnderBaseChange.diagonal CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource AlgebraicGeometry.Flat.instHasRingHomPropertyFlat
instIsZariskiLocalAtSource 📖	mathematical	—	AlgebraicGeometry.IsZariskiLocalAtSource AlgebraicGeometry.WeaklyEtale	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks weaklyEtale_eq_flat_inf_diagonal_flat CategoryTheory.MorphismProperty.IsLocalAtSource.inf AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource AlgebraicGeometry.Flat.instHasRingHomPropertyFlat AlgebraicGeometry.instIsZariskiLocalAtSourceDiagonalSchemeOfHasOfPostcompPropertyOfRespectsRightIsOpenImmersion AlgebraicGeometry.instHasOfPostcompPropertySchemeIsOpenImmersionOfIsStableUnderBaseChange AlgebraicGeometry.Flat.isStableUnderBaseChange CategoryTheory.MorphismProperty.Respects.toRespectsRight AlgebraicGeometry.Flat.instRespectsSchemeIsOpenImmersion
instIsZariskiLocalAtTarget 📖	mathematical	—	AlgebraicGeometry.IsZariskiLocalAtTarget AlgebraicGeometry.WeaklyEtale	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks weaklyEtale_eq_flat_inf_diagonal_flat CategoryTheory.MorphismProperty.IsLocalAtTarget.inf AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget AlgebraicGeometry.Flat.instHasRingHomPropertyFlat AlgebraicGeometry.instIsZariskiLocalAtTargetDiagonalScheme
instMorphismRestrict 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale AlgebraicGeometry.Scheme.Opens.toScheme CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' AlgebraicGeometry.morphismRestrict	—	AlgebraicGeometry.IsZariskiLocalAtTarget.restrict instIsZariskiLocalAtTarget
instOfEtale 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale	—	AlgebraicGeometry.instFlatOfSmooth AlgebraicGeometry.Etale.instSmooth AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.Flat.instOfIsOpenImmersion AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal AlgebraicGeometry.Etale.instFormallyUnramified AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth
instResLE 📖	mathematical	AlgebraicGeometry.Scheme.Opens Preorder.toLE PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier CategoryTheory.Functor.obj Preorder.smallCategory TopologicalSpace.Opens TopCat.str TopologicalSpace.Opens.map AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom'	AlgebraicGeometry.WeaklyEtale AlgebraicGeometry.Scheme.Opens.toScheme AlgebraicGeometry.Scheme.Hom.resLE	—	instCompScheme instOfEtale AlgebraicGeometry.Etale.instOfIsOpenImmersion AlgebraicGeometry.instIsOpenImmersionHomOfLE instMorphismRestrict
instRespectsIsoScheme 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.WeaklyEtale	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks weaklyEtale_eq_flat_inf_diagonal_flat CategoryTheory.MorphismProperty.inf CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource AlgebraicGeometry.Flat.instHasRingHomPropertyFlat CategoryTheory.MorphismProperty.RespectsIso.diagonal
instSndScheme 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale CategoryTheory.Limits.pullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeScheme
of_comp 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale	—	CategoryTheory.MorphismProperty.of_postcomp instHasOfPostcompPropertyScheme
weaklyEtale_eq_flat_inf_diagonal_flat 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra AlgebraicGeometry.Flat CategoryTheory.MorphismProperty.diagonal AlgebraicGeometry.Scheme.Pullback.instHasPullbacks	—	AlgebraicGeometry.Scheme.Pullback.instHasPullbacks AlgebraicGeometry.weaklyEtale_iff

---

← Back to Index