Étale equivalence of hypersurfaces of maximal contact #
The second half of [Kol07, Definition 91] calls two hypersurfaces of maximal contact H and H'
étale equivalent with respect to (X, I, E) when there are étale surjections ψ, ψ' : U ⇉ X
with (1′) ψ⁻¹(H) = ψ'⁻¹(H'), (2′) ψ^*(I) = ψ'^*(I), (3′) ψ⁻¹(Eⁱ) = ψ'⁻¹(Eⁱ) for every
component Eⁱ of E, and (4′) ψ^*(h) − ψ'^*(h) ∈ MC ψ^*(I) for every function h on X.
Conventions. The definition is stated for étale maps ψ, ψ' whose images each contain the
cosupport cosupp(I, m) = {x | ord_x I ≥ m} (AlgebraicGeometry.EtaleImagePair X (cosupp I m))
in place of Kollár's étale surjections. With surjections, Theorem 92 would be false: for
X = 𝔸¹, I = (xᵐ), H = V(x) and H' = V(x(x − 1)), every hypothesis of Theorem 92 holds,
but no étale surjections satisfy (1′) and (2′), since a point u of U over 1 along ψ' lies
over H, hence over 0, along ψ by (1′), so ψ^*(xᵐ) vanishes at u, and then by (2′) so
does ψ'^*(xᵐ), which is impossible at 1. What the proof of Theorem 92 constructs are étale
neighbourhoods whose images cover the cosupport, and that is also what the functoriality argument
of [Kol07, Theorem 103, Step 2.3] uses. Condition (4′) is stated as the equality of morphisms
ψ ∘ ι = ψ' ∘ ι on the closed subscheme V(MC(ψ^*I)) (AgreeOn). Kollár's ψ, ψ' are
morphisms of k-varieties: the field comp_eq (ψ ≫ f = ψ' ≫ f) records it, so that
ψ̂' ∘ ψ̂⁻¹ is a k-automorphism of Ô_{X,p} (FormallyEquivalentAt,
Hironaka/Resolution/Algebraic/MaximalContact/EtaleToFormal.lean).
AgreeOn ψ ψ' M:ψandψ'agree on the closed subschemeV(M) ⊆ U.EtaleEquiv f I m E H H': the étale equivalence datum, anEtaleImagePair X (cosupp I m)with the conditions (1′)–(4′) andψ ≫ f = ψ' ≫ f.MC_comap_of_etale: [Kol07, Lemma 74 (4)] forMC,MC(ψ^*I) = ψ^*MC(I)for an étaleψ(derivativeIter_comap_of_smooth), so (4′) may be read with either ideal.EtaleEquiv.refl:His étale equivalent to itself throughU = X,ψ = ψ' = 𝟙 X.
The morphisms ψ, ψ' : U ⟶ X agree on the closed subscheme V(M): ψ ∘ ι = ψ' ∘ ι for
the closed immersion ι : V(M) ⟶ U. This is the form in which the condition (4′) of
[Kol07, Definition 91] is stated.
Equations
Instances For
AgreeOn unfolded.
[Kol07, Definition 91], second half, with images containing the cosupport in place of
surjections: H and H' are étale equivalent with respect to (X, I, E), for the mark m,
through the étale pair ψ, ψ' : U ⟶ X whose images each contain cosupp(I, m) = {x | ord_x I ≥ m}
(EtaleImagePair), when (1′) ψ⁻¹(H) = ψ'⁻¹(H'), (2′) ψ^*I = ψ'^*I, (3′) ψ⁻¹(Eⁱ) = ψ'⁻¹(Eⁱ)
for every component Eⁱ of E, and (4′) ψ and ψ' agree on V(MC(ψ^*I)); ψ and ψ' are
morphisms of k-schemes (ψ ≫ f = ψ' ≫ f, Kollár's varieties over k). Inverse images of closed
subschemes are Mathlib's comap of ideal sheaves.
- comp_eq : CategoryTheory.CategoryStruct.comp self.ψ f = CategoryTheory.CategoryStruct.comp self.ψ' f
ψandψ'are morphisms ofk-schemes. (1′)
ψ⁻¹(H) = ψ'⁻¹(H').(2′)
ψ^*(I) = ψ'^*(I).(3′)
ψ⁻¹(Eⁱ) = ψ'⁻¹(Eⁱ)for every component.(4′)
ψandψ'agree on the closed subschemeV(MC(ψ^*I))(thek-structure ofUisψ ≫ f).
Instances For
The conditions (1′)–(4′) of an étale equivalence, bundled.
In place of Kollár's "étale surjections": the images of ψ and ψ' each contain the
cosupport cosupp(I, m).
ψ and ψ' are morphisms over k: the field comp_eq restated.
[Kol07, Lemma 74 (4)] for MC, "MC(ψ^*I) = ψ^*MC(I)": for X smooth over k and
ψ : U ⟶ X étale, the maximal contact ideal of the pulled-back ideal (for the k-structure
ψ ≫ f of U) is the pullback of the maximal contact ideal (derivativeIter_comap_of_smooth).
The trivial instance: H is étale equivalent to itself through U = X and ψ = ψ' = 𝟙 X.
Equations
- One or more equations did not get rendered due to their size.