The maximal contact classes satisfy the hypotheses of Theorem 105

The global case of the proof of Theorem 103 [Kol07, 104, Step 3] globalizes the maximal contact case by [Kol07, Theorem 105] with M = coproducts of open immersions, GT = GT_{n,m} (triples with dim X = n, max-ord I ≤ m) and LT = LT_{n,m} (those admitting a global smooth hypersurface of maximal contact). This module proves that these classes (Hironaka/Resolution/Algebraic/Kol07/MaximalContactClasses.lean) satisfy the hypotheses (2)(i)–(ii) of Theorem 105, the local existence resting on the local existence of hypersurfaces of maximal contact [Kol07, Theorem 80 (2)].

• The classes (orderClass_iff, maximalContactClass_iff, MaximalContactClass.orderClass): unfoldings and LT ⊆ GT.
• Below the mark (hasMaximalContact_of_maxOrd_lt): when max-ord I < m, MC(I) = D^{m-1}(I) has order 0 at every point (ord_MC_eq_zero, a characteristic-zero fact), so it is the unit ideal and the empty hypersurface H = 𝒪_X, a smooth divisor (isSmoothDivisor_top), is of maximal contact.
• Closure under finite disjoint unions (Theorem 105 (2)(ii); "this condition is also preserved under disjoint unions", [Kol07, 104, Step 2]): the dimension is local on the source, so a finite coproduct of n-dimensional pieces is n-dimensional (closedUnderSigma_hasDim, via IsZariskiLocalAtSource.sigmaDesc and the isomorphism ∐ Xⁱ ≅ X); max-ord ≤ m is closedUnderSigma_maxOrd_le; and the union H^* = ∐ H^(j), realised as the intersection ⨅ j, (H^(j)).map (ι j) of the ideals of the closed pieces, restricts to H^(j) on the j-th piece (each ι j is a closed immersion, an open immersion with closed image, the complement being the union of the other pieces; the direct image of H^(i) along ι i restricts to the unit ideal on a different piece; and inverse images along open immersions commute with finite intersections), so it is a smooth divisor (isSmoothDivisor_of_forall_comap) and lies in MC(I) (le_of_forall_comap_le, with MC(I|_{Xʲ}) = MC(I)|_{Xʲ} by derivativeIter_comap_of_smooth).
• Closure under pullback along coproducts of open immersions (the hypothesis LocalCoversFibreClosed of the descent): such a morphism is étale, hence of relative dimension 0, so the dimension persists; the order of g^* I at a point is the order of I at its image (through the summand containing the point); g^{-1} H is a smooth divisor (restriction along each summand's open immersion) inside MC(g^* I) = g^* MC(I).
• Local existence (Theorem 105 (2)(i); exists_isPullbackOf_maximalContactClass): at a point where max-ord I < m the triple itself, along the identity, is a local triple (below the mark); at a point where max-ord I = m, [Kol07, Theorem 80 (2)] (exists_opens_isSmoothDivisor_isMaximalContact) gives an open U ∋ x with a smooth divisor of maximal contact H; an affine V ≤ U around x (exists_isAffineOpen_mem_and_subset) makes T|_V a triple (Triple.pullback along the open immersion V.ι, the class hypotheses by composition and affineness), V.ι is a coproduct of open immersions with one summand, and H|_V is a smooth divisor of maximal contact for T|_V.
• The assembly and the instance (globalizationData_of_exists_isPullbackOf, globalizationData_maximalContact): the local existence together with (2)(ii) is the GlobalizationData.

The classes

theorem AlgebraicGeometry.Triple.orderClass_iff {k : Type u} [Field k] (n m : ℕ) (T : Triple k) : OrderClass n m T ↔ T.HasDim n ∧ T.I.maxOrd ≤ ↑m

The class GT_{n,m} of [Kol07, Theorem 103], unfolded.

theorem AlgebraicGeometry.Triple.maximalContactClass_iff {k : Type u} [Field k] (n m : ℕ) (T : Triple k) : MaximalContactClass n m T ↔ OrderClass n m T ∧ T.HasMaximalContact m

The class LT_{n,m} of [Kol07, 104, Step 3], unfolded.

theorem AlgebraicGeometry.Triple.MaximalContactClass.orderClass {k : Type u} [Field k] {n m : ℕ} {T : Triple k} (h : MaximalContactClass n m T) : OrderClass n m T

LT_{n,m} ⊆ GT_{n,m}.

theorem AlgebraicGeometry.Triple.hasMaximalContact_of_maxOrd_lt {k : Type u} [Field k] [CharZero k] (T : Triple k) {m : ℕ} (h : T.I.maxOrd < ↑m) : T.HasMaximalContact m

Below the mark the empty hypersurface H = 𝒪_X is a smooth divisor of maximal contact, since MC(I) = 𝒪_X (ord_MC_eq_zero). Not in the sources; the case max-ord I < m, where Kollár's functor does nothing.

Closure under finite disjoint unions (Theorem 105 (2)(ii))

theorem AlgebraicGeometry.Triple.closedUnderSigma_hasDim {k : Type u} [Field k] (n : ℕ) : ClosedUnderSigma fun (T : Triple k) => T.HasDim n

The dimension is local on the source, so dim X = n is closed under finite disjoint unions (the disjoint union X^* = ∐ X^(j) of [Kol07, 104, Step 3]).

theorem AlgebraicGeometry.Triple.closedUnderSigma_orderClass {k : Type u} [Field k] (n m : ℕ) : ClosedUnderSigma (OrderClass n m)

GT_{n,m} is closed under finite disjoint unions (closedUnderSigma_maxOrd_le for the order).

theorem AlgebraicGeometry.Triple.IsSigmaOf.isMaximalContact_sigma {k : Type u} [Field k] {σ : Type u} [Finite σ] {T : Triple k} {Ts : σ → Triple k} {ι : (i : σ) → (Ts i).X.left ⟶ T.X.left} (h : T.IsSigmaOf Ts ι) {m : ℕ} (H : (i : σ) → (Ts i).X.left.IdealSheafData) (hs : ∀ (i : σ), IsSmoothDivisor (H i)) (hmc : ∀ (i : σ), Scheme.IdealSheafData.IsMaximalContact ((Ts i).X.left ↘ Spec ↧k) (Ts i).I m (H i)) : IsSmoothDivisor (⨅ (i : σ), (H i).map (ι i)) ∧ Scheme.IdealSheafData.IsMaximalContact (T.X.left ↘ Spec ↧k) T.I m (⨅ (i : σ), (H i).map (ι i))

"H^* := ∐ H^(j) ⊂ ∐ X^(j) =: X^* is a smooth hypersurface of maximal contact" [Kol07, 104, Step 3]: the union of the pieces' hypersurfaces is a smooth hypersurface of maximal contact on the disjoint union.

theorem AlgebraicGeometry.Triple.closedUnderSigma_hasMaximalContact {k : Type u} [Field k] (m : ℕ) : ClosedUnderSigma fun (T : Triple k) => T.HasMaximalContact m

Admitting a global smooth hypersurface of maximal contact is closed under finite disjoint unions ("this condition is also preserved under disjoint unions", [Kol07, 104, Step 2]).

theorem AlgebraicGeometry.Triple.closedUnderSigma_maximalContactClass {k : Type u} [Field k] (n m : ℕ) : ClosedUnderSigma (MaximalContactClass n m)

Hypothesis (2)(ii) of [Kol07, Theorem 105] for the instance: LT_{n,m} is closed under finite disjoint unions.

Closure under pullback along coproducts of open immersions

theorem AlgebraicGeometry.Triple.HasDim.isPullbackOf {k : Type u} [Field k] {T T' : Triple k} {g : T'.X.left ⟶ T.X.left} {n : ℕ} (hT : T.HasDim n) (hg : openImmersionCoprods g) (hT' : T'.IsPullbackOf T g) : T'.HasDim n

Pulling back along a coproduct of open immersions (étale, hence of relative dimension 0) keeps the dimension.

theorem AlgebraicGeometry.Triple.OrderClass.isPullbackOf {k : Type u} [Field k] {T T' : Triple k} {g : T'.X.left ⟶ T.X.left} {n m : ℕ} (hT : OrderClass n m T) (hg : openImmersionCoprods g) (hT' : T'.IsPullbackOf T g) : OrderClass n m T'

GT_{n,m} is closed under pullback along coproducts of open immersions (ord_comap_of_isOpenImmersion for the order).

theorem AlgebraicGeometry.Triple.HasMaximalContact.isPullbackOf {k : Type u} [Field k] {T T' : Triple k} {g : T'.X.left ⟶ T.X.left} {m : ℕ} (hT : T.HasMaximalContact m) (hg : openImmersionCoprods g) (hT' : T'.IsPullbackOf T g) : T'.HasMaximalContact m

A global smooth hypersurface of maximal contact restricts along a coproduct of open immersions: g^{-1} H is a smooth divisor on each summand and MC(g^* I) = g^* MC(I) (derivativeIter_comap_of_smooth).

theorem AlgebraicGeometry.Triple.MaximalContactClass.isPullbackOf {k : Type u} [Field k] {T T' : Triple k} {g : T'.X.left ⟶ T.X.left} {n m : ℕ} (hT : MaximalContactClass n m T) (hg : openImmersionCoprods g) (hT' : T'.IsPullbackOf T g) : MaximalContactClass n m T'

LT_{n,m} is closed under pullback along coproducts of open immersions (the hypothesis LocalCoversFibreClosed of the descent, for this instance).

The assembly

theorem AlgebraicGeometry.Triple.globalizationData_of_exists_isPullbackOf {k : Type u} [Field k] (n m : ℕ) (h : ∀ (T : Triple k), OrderClass n m T → ∀ (x : ↥T.X.left), ∃ (T' : Triple k) (g : T'.X.left ⟶ T.X.left), openImmersionCoprods g ∧ x ∈ Set.range ⇑g ∧ T'.IsPullbackOf T g ∧ MaximalContactClass n m T') : GlobalizationData openImmersionCoprods (OrderClass n m) (MaximalContactClass n m)

The local existence as a hypothesis and the closure under disjoint unions make the data (2) of [Kol07, Theorem 105].

Local existence (Theorem 105 (2)(i)) and the instance

theorem AlgebraicGeometry.Triple.exists_isPullbackOf_maximalContactClass {k : Type u} [Field k] [CharZero k] (n m : ℕ) (T : Triple k) (hT : OrderClass n m T) (x : ↥T.X.left) : ∃ (T' : Triple k) (g : T'.X.left ⟶ T.X.left), openImmersionCoprods g ∧ x ∈ Set.range ⇑g ∧ T'.IsPullbackOf T g ∧ MaximalContactClass n m T'

Hypothesis (2)(i) of [Kol07, Theorem 105] for the instance: every point of a GT_{n,m}-triple lies in the image of a coproduct of open immersions from an LT_{n,m}-triple carrying the pullback data. At a point of order m this is the local existence of a smooth hypersurface of maximal contact [Kol07, Theorem 80 (2)]; below the mark, hasMaximalContact_of_maxOrd_lt.

theorem AlgebraicGeometry.Triple.globalizationData_maximalContact {k : Type u} [Field k] [CharZero k] (n m : ℕ) : GlobalizationData openImmersionCoprods (OrderClass n m) (MaximalContactClass n m)

The instance of [Kol07, Theorem 105] used in the global case of the proof of Theorem 103 [Kol07, 104, Step 3]: M = coproducts of open immersions, GT = GT_{n,m} and LT = LT_{n,m} satisfy the hypotheses (2)(i)–(ii).