theorem Separatedness.affine_isSeparated (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsAffine X] : X.IsSeparated

Any affine scheme is separated.

theorem Separatedness.prop9_forward {X : AlgebraicGeometry.Scheme} [X.IsSeparated] {U V : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) (hV : AlgebraicGeometry.IsAffineOpen V) : AlgebraicGeometry.IsAffineOpen (U ⊓ V)

Forward direction of Prop 9 (separatedness via affine opens): in a separated scheme X, the intersection of two affine open subschemes is affine.

theorem Separatedness.affine_diagonal_iff_affine_intersection {X : AlgebraicGeometry.Scheme} : AlgebraicGeometry.IsAffineHom (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X)) ↔ ∀ (U V : X.Opens), AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen V → AlgebraicGeometry.IsAffineOpen (U ⊓ V)

The diagonal of X is an affine morphism iff intersections of affine opens in X are affine.

theorem Separatedness.prop9_separated_iff {X : AlgebraicGeometry.Scheme} : X.IsSeparated ↔ (∀ (U V : X.Opens), AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen V → AlgebraicGeometry.IsAffineOpen (U ⊓ V)) ∧ ∀ (W : (CategoryTheory.Limits.pullback (CategoryTheory.Limits.terminal.from X) (CategoryTheory.Limits.terminal.from X)).Opens), AlgebraicGeometry.IsAffineOpen W → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app (CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.terminal.from X)) W))

Proposition 9 (separatedness criterion): X is separated iff (i) intersections of affine opens are affine, and (ii) the diagonal map induces surjections on affine open stalks.

theorem Separatedness.tmul_one_sub_one_tmul_mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (a b : A) : (a * b) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (a * b) = a ⊗ₜ[R] 1 * (b ⊗ₜ[R] 1 - 1 ⊗ₜ[R] b) + (a ⊗ₜ[R] 1 - 1 ⊗ₜ[R] a) * 1 ⊗ₜ[R] b

Tensor product derivation rule for multiplication: (ab) ⊗ 1 − 1 ⊗ (ab) = (a ⊗ 1)(b ⊗ 1 − 1 ⊗ b) + (a ⊗ 1 − 1 ⊗ a)(1 ⊗ b).

theorem Separatedness.tmul_one_sub_one_tmul_add {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (a b : A) : (a + b) ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (a + b) = a ⊗ₜ[R] 1 - 1 ⊗ₜ[R] a + (b ⊗ₜ[R] 1 - 1 ⊗ₜ[R] b)

Additivity of the a ↦ a ⊗ 1 − 1 ⊗ a map.

theorem Separatedness.tmul_one_sub_one_tmul_algebraMap {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (r : R) : (algebraMap R A) r ⊗ₜ[R] 1 - 1 ⊗ₜ[R] (algebraMap R A) r = 0

Elements coming from the base ring vanish under a ↦ a ⊗ 1 − 1 ⊗ a.