5.2. Weakly étale morphisms of schemes
Definition5.2.1
Group: The pro-étale site of a scheme and its basic properties, including the comparison with étale cohomology, following Sections 4 and 5 of Bhatt–Scholze. (36)
- Lemma 5.1.1
- Lemma 5.2.2
- Lemma 5.2.3
- Lemma 5.2.4
- Definition 5.3.1
- Lemma 5.3.2
- Definition 5.3.3
- Definition 5.3.4
- Theorem 5.3.5
- Proposition 5.3.6
- Definition 5.3.7
- Proposition 5.3.8
- Definition 5.3.1.1
- Lemma 5.3.1.2
- Definition 5.3.1.3
- Proposition 5.3.1.4
- Corollary 5.3.1.5
- Corollary 5.3.1.6
- Proposition 5.3.1.7
- Proposition 5.3.2.1
- Corollary 5.3.2.2
- Definition 5.4.1
- Lemma 5.4.2
- Lemma 5.4.3
- Lemma 5.4.4
- Proposition 5.4.5
- Corollary 5.4.6
- Corollary 5.4.7
- Corollary 5.4.8
- Definition 5.4.9
- Corollary 5.4.10
- Lemma 5.4.11
- Proposition 5.4.12
- Corollary 5.4.13
- Definition 5.4.14
- Theorem 5.4.15
Used by 4
Associated Lean declarations
-
AlgebraicGeometry.WeaklyEtale[complete]
A map f \colon Y \to X is weakly étale if f is flat and
\Delta_f\colon Y \to Y \times_{X} Y is flat.
(Bhatt–Scholze, Definition 4.1.1)
Lean code for Definition5.2.1●1 definition
Associated Lean declarations
-
AlgebraicGeometry.WeaklyEtale[complete]
Associated Lean declarations
-
AlgebraicGeometry.WeaklyEtale[complete]
-
classdefined in Mathlib/AlgebraicGeometry/Morphisms/WeaklyEtale.leancomplete
class AlgebraicGeometry.WeaklyEtale.{u} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop
class AlgebraicGeometry.WeaklyEtale.{u} {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop
A morphism is weakly étale if it is flat and the diagonal map is flat.
Methods
flat : AlgebraicGeometry.Flat f
flat_diagonal : AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.diagonal f)
Lemma5.2.2
Group: The pro-étale site of a scheme and its basic properties, including the comparison with étale cohomology, following Sections 4 and 5 of Bhatt–Scholze. (36)
- Lemma 5.1.1
- Definition 5.2.1
- Lemma 5.2.3
- Lemma 5.2.4
- Definition 5.3.1
- Lemma 5.3.2
- Definition 5.3.3
- Definition 5.3.4
- Theorem 5.3.5
- Proposition 5.3.6
- Definition 5.3.7
- Proposition 5.3.8
- Definition 5.3.1.1
- Lemma 5.3.1.2
- Definition 5.3.1.3
- Proposition 5.3.1.4
- Corollary 5.3.1.5
- Corollary 5.3.1.6
- Proposition 5.3.1.7
- Proposition 5.3.2.1
- Corollary 5.3.2.2
- Definition 5.4.1
- Lemma 5.4.2
- Lemma 5.4.3
- Lemma 5.4.4
- Proposition 5.4.5
- Corollary 5.4.6
- Corollary 5.4.7
- Corollary 5.4.8
- Definition 5.4.9
- Corollary 5.4.10
- Lemma 5.4.11
- Proposition 5.4.12
- Corollary 5.4.13
- Definition 5.4.14
- Theorem 5.4.15
Statement uses 2
Associated Lean declarations
(Local property of weakly étale morphisms.) f \colon Y \to X is weakly étale
if and only if for every affine open U of Y and every affine open V of
X with f(U) \subset V, the induced ring homomorphism
\Gamma(X, V) \to \Gamma(Y, U) is weakly étale.
Lean code for Lemma5.2.2●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theoremdefined in Proetale/Morphisms/WeaklyEtale.leancomplete
theorem AlgebraicGeometry.WeaklyEtale.hasRingHomProperty.{u} : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.WeaklyEtale fun {R S} [CommRing R] [CommRing S] => RingHom.WeaklyEtale
theorem AlgebraicGeometry.WeaklyEtale.hasRingHomProperty.{u} : AlgebraicGeometry.HasRingHomProperty @AlgebraicGeometry.WeaklyEtale fun {R S} [CommRing R] [CommRing S] => RingHom.WeaklyEtale
`WeaklyEtale` is induced by the ring-homomorphism property `RingHom.WeaklyEtale`, in the sense that a morphism `f : X ⟶ Y` of schemes is weakly étale iff for every affine open `U ⊆ Y` and every affine open `V ⊆ X` with `f(V) ⊆ U`, the induced ring homomorphism `Γ(Y, U) → Γ(X, V)` is weakly étale.
Proof for Lemma 5.2.2
uses 0
Weakly étale morphisms of schemes are local on source and on target for the Zariski topology, so the property descends to affine opens. There it matches the ring-theoretic definition via the characterisation of weakly étale algebras (Definition 2.1.1).
Lemma5.2.3
Group: The pro-étale site of a scheme and its basic properties, including the comparison with étale cohomology, following Sections 4 and 5 of Bhatt–Scholze. (36)
- Lemma 5.1.1
- Definition 5.2.1
- Lemma 5.2.2
- Lemma 5.2.4
- Definition 5.3.1
- Lemma 5.3.2
- Definition 5.3.3
- Definition 5.3.4
- Theorem 5.3.5
- Proposition 5.3.6
- Definition 5.3.7
- Proposition 5.3.8
- Definition 5.3.1.1
- Lemma 5.3.1.2
- Definition 5.3.1.3
- Proposition 5.3.1.4
- Corollary 5.3.1.5
- Corollary 5.3.1.6
- Proposition 5.3.1.7
- Proposition 5.3.2.1
- Corollary 5.3.2.2
- Definition 5.4.1
- Lemma 5.4.2
- Lemma 5.4.3
- Lemma 5.4.4
- Proposition 5.4.5
- Corollary 5.4.6
- Corollary 5.4.7
- Corollary 5.4.8
- Definition 5.4.9
- Corollary 5.4.10
- Lemma 5.4.11
- Proposition 5.4.12
- Corollary 5.4.13
- Definition 5.4.14
- Theorem 5.4.15
Lean status
- No associated Lean code or declarations.
Etale morphisms are weakly étale.
Proof for Lemma 5.2.3
uses 0
Any étale morphism is flat and its diagonal is an open immersion, hence flat.
Lemma5.2.4
Group: The pro-étale site of a scheme and its basic properties, including the comparison with étale cohomology, following Sections 4 and 5 of Bhatt–Scholze. (36)
- Lemma 5.1.1
- Definition 5.2.1
- Lemma 5.2.2
- Lemma 5.2.3
- Definition 5.3.1
- Lemma 5.3.2
- Definition 5.3.3
- Definition 5.3.4
- Theorem 5.3.5
- Proposition 5.3.6
- Definition 5.3.7
- Proposition 5.3.8
- Definition 5.3.1.1
- Lemma 5.3.1.2
- Definition 5.3.1.3
- Proposition 5.3.1.4
- Corollary 5.3.1.5
- Corollary 5.3.1.6
- Proposition 5.3.1.7
- Proposition 5.3.2.1
- Corollary 5.3.2.2
- Definition 5.4.1
- Lemma 5.4.2
- Lemma 5.4.3
- Lemma 5.4.4
- Proposition 5.4.5
- Corollary 5.4.6
- Corollary 5.4.7
- Corollary 5.4.8
- Definition 5.4.9
- Corollary 5.4.10
- Lemma 5.4.11
- Proposition 5.4.12
- Corollary 5.4.13
- Definition 5.4.14
- Theorem 5.4.15
Lean status
- No associated Lean code or declarations.
Weakly étale is stable under composition and base change. (Bhatt–Scholze, Lemma 4.1.6)
Proof for Lemma 5.2.4
uses 0
This follows because flat is stable under composition and base change.