theorem closedEmbedding_prodMap {X₁ : Type u_1} {Y₁ : Type u_2} {X₂ : Type u_3} {Y₂ : Type u_4} [TopologicalSpace X₁] [TopologicalSpace Y₁] [TopologicalSpace X₂] [TopologicalSpace Y₂] {f : X₁ → Y₁} {g : X₂ → Y₂} (hf : Topology.IsClosedEmbedding f) (hg : Topology.IsClosedEmbedding g) : Topology.IsClosedEmbedding (Prod.map f g)

The product of two closed embeddings is a closed embedding: if f : X₁ → Y₁ and g : X₂ → Y₂ are closed embeddings, then so is Prod.map f g : X₁ × X₂ → Y₁ × Y₂. This is the topological input to showing that products of separated schemes are separated.

theorem isClosed_prod_of_isClosed {Y₁ : Type u_1} {Y₂ : Type u_2} [TopologicalSpace Y₁] [TopologicalSpace Y₂] {S₁ : Set Y₁} {S₂ : Set Y₂} (h₁ : IsClosed S₁) (h₂ : IsClosed S₂) : IsClosed (S₁ ×ˢ S₂)

A product of two closed sets is closed in the product topology.

theorem tensorProduct_map_surjective {R : Type u_1} {M : Type u_2} {N : Type u_3} {M' : Type u_4} {N' : Type u_5} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [AddCommMonoid M'] [Module R M'] [AddCommMonoid N'] [Module R N'] {f : M →ₗ[R] M'} {g : N →ₗ[R] N'} (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) : Function.Surjective ⇑(TensorProduct.map f g)

The tensor product of two surjective linear maps is surjective: if f : M → M' and g : N → N' are surjective, then f ⊗ g : M ⊗ N → M' ⊗ N' is surjective. This is the algebraic counterpart of the closed embedding fact for products of affine schemes.

theorem algHom_tensorProduct_map_surjective {R : Type u_1} {A₁ : Type u_2} {B₁ : Type u_3} {A₂ : Type u_4} {B₂ : Type u_5} [CommSemiring R] [CommSemiring A₁] [CommSemiring B₁] [CommSemiring A₂] [CommSemiring B₂] [Algebra R A₁] [Algebra R B₁] [Algebra R A₂] [Algebra R B₂] {φ : A₁ →ₐ[R] B₁} {ψ : A₂ →ₐ[R] B₂} (hφ : Function.Surjective ⇑φ) (hψ : Function.Surjective ⇑ψ) : Function.Surjective ⇑(Algebra.TensorProduct.map φ ψ)

The tensor product of two surjective R-algebra homomorphisms is surjective. Used to show that closed immersions are preserved under taking products of schemes over a base.

theorem ringHom_eq_of_crossRatio {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [NoZeroDivisors B] (f g : A →+* B) {s : A} (hgs : g s ≠ 0) (h : ∀ (a : A), f a * g s = g a * f s) : f = g

Two ring homomorphisms f, g : A → B into a domain B that satisfy the cross-ratio relation f a · g s = g a · f s for all a, with g s ≠ 0, are equal. A separation-style cancellation lemma used in the proof that the diagonal of a variety is closed.

theorem ringHom_eq_of_eq_on_base {R : Type u_1} [CommSemiring R] (M : Submonoid R) {S : Type u_2} [CommSemiring S] [Algebra R S] [IsLocalization M S] {P : Type u_3} [Semiring P] (j k : S →+* P) (h : ∀ (a : R), j ((algebraMap R S) a) = k ((algebraMap R S) a)) : j = k

Two ring homomorphisms out of a localization S = M⁻¹R are equal as soon as they agree on the image of the base ring R. The universal property of localization.

theorem fieldHom_eq_of_eq_on_domain {A : Type u_1} [CommRing A] [IsDomain A] {K : Type u_2} [Field K] [Algebra A K] [IsFractionRing A K] {L : Type u_3} [Field L] (f g : K →+* L) (h : ∀ (a : A), f ((algebraMap A K) a) = g ((algebraMap A K) a)) : f = g

Two field homomorphisms out of a fraction field K = Frac(A) are equal as soon as they agree on the image of the domain A. Specialization of the localization universal property to fraction fields.