Structures · Geometry
AlgebraicGeometry.Etale
A morphism of schemes f : X ⟶ Y is étale if for each affine U ⊆ Y and
V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is étale.
- Shape
- One type argument · adds etale_appLE
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Forgetful instances
Every AlgebraicGeometry.Etale is also a
Concrete types that are instances5
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Hom.fiber
- AlgebraicGeometry.Scheme.Opens.toScheme
- CategoryTheory.PreZeroHypercover.X
- CategoryTheory.Comma.left
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- AlgebraicGeometry.Etale.etale_appLE
- AlgebraicGeometry.Scheme.exists_fac_of_etale_of_isSepClosed
- AlgebraicGeometry.Etale.instFstScheme
- AlgebraicGeometry.Scheme.AffineEtale.mk_right_as
- AlgebraicGeometry.Etale.etale_comp
- AlgebraicGeometry.Etale.instMorphismRestrict
- AlgebraicGeometry.Etale.instSmoothOfRelativeDimensionOfNatNat
- AlgebraicGeometry.Scheme.AffineEtale.mk_left
- AlgebraicGeometry.Etale.instResLE
- AlgebraicGeometry.Scheme.Etale.mk.congr_simp
- AlgebraicGeometry.Etale.of_comp
- AlgebraicGeometry.WeaklyEtale.instOfEtale
- AlgebraicGeometry.Etale.instSndScheme
- AlgebraicGeometry.Etale.instSmooth
- AlgebraicGeometry.Scheme.Etale.forget_mk
- AlgebraicGeometry.Scheme.Hom.etale_appLE
- AlgebraicGeometry.Etale.instFormallyUnramified
- AlgebraicGeometry.Scheme.AffineEtale.mk_hom
- AlgebraicGeometry.Scheme.instEtaleFiberToSpecResidueField