Ranks of finite flat closed subschemes

An inclusion of closed subschemes finite and flat over the same base is equality when their rank functions agree. In ideal-sheaf notation the direction of containment is reversed: I ≤ J gives the closed immersion J.subscheme ⟶ I.subscheme.

The intersection of two closed subschemes V(I) and V(J) of X can be cut out inside either of them: as the inverse image V(I) ∩ V(J) = V(I.comap ι_J) of V(I) in V(J), or as the inverse image V(J.comap ι_I) of V(J) in V(I). Both are the fibre product V(I) ×_X V(J), so when V(I) and V(J) map to a base compatibly on their intersection, the two descriptions have the same rank over the base (Scheme.IdealSheafData.finrank_comap_subschemeι_comm). For two curves on a surface, this is the symmetry of the length of their scheme-theoretic intersection.

Main results

• AlgebraicGeometry.Scheme.IdealSheafData.eq_of_le_of_finrank_eq: comparable ideal sheaves cutting out finite flat schemes of the same rank are equal;
• AlgebraicGeometry.Scheme.IdealSheafData.finrank_comap_subschemeι_comm: the rank of V(I) ∩ V(J) does not depend on which of the two subschemes it is cut out in.

theorem AlgebraicGeometry.Scheme.IdealSheafData.eq_of_le_of_finrank_eq {X S : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (f : X ⟶ S) [IsFinite (CategoryTheory.CategoryStruct.comp I.subschemeι f)] [Flat (CategoryTheory.CategoryStruct.comp I.subschemeι f)] [Flat (CategoryTheory.CategoryStruct.comp J.subschemeι f)] (hrank : Hom.finrank (CategoryTheory.CategoryStruct.comp I.subschemeι f) = Hom.finrank (CategoryTheory.CategoryStruct.comp J.subschemeι f)) : I = J

Comparable ideal sheaves cutting out finite flat schemes of the same rank over the base are equal.

theorem AlgebraicGeometry.Scheme.IdealSheafData.finrank_comap_subschemeι_comm {X S : Scheme} {I J : X.IdealSheafData} (f : I.subscheme ⟶ S) (g : J.subscheme ⟶ S) (w : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst J.subschemeι I.subschemeι) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd J.subschemeι I.subschemeι) f) [IsFinite (CategoryTheory.CategoryStruct.comp (J.comap I.subschemeι).subschemeι f)] [Flat (CategoryTheory.CategoryStruct.comp (J.comap I.subschemeι).subschemeι f)] : Hom.finrank (CategoryTheory.CategoryStruct.comp (I.comap J.subschemeι).subschemeι g) = Hom.finrank (CategoryTheory.CategoryStruct.comp (J.comap I.subschemeι).subschemeι f)

The intersection of two closed subschemes is symmetric. Let V(I) and V(J) be closed subschemes of X mapping to a base S by f and g, compatibly on their fibre product. Then the inverse image of V(I) in V(J) and the inverse image of V(J) in V(I), both the intersection V(I) ∩ V(J), have the same rank over S when one of them is finite and flat over S.