Universal homeomorphisms of schemes

A universal homeomorphism is a scheme morphism whose every base change is a homeomorphism on underlying spaces. Such maps are surjective, universally injective and universally closed. Conversely, these three properties suffice. Equivalently, a universal homeomorphism is an integral, universally injective, surjective morphism.

This criterion applies to Frobenius without imposing finiteness or reducedness assumptions.

References

• TauCetiProject/TauCeti#18102 by @sqrt-of-2, whose class construction via mk_iff, universally-closed criterion, and integrality proof via isAffineHom_of_isInducing this module follows.
• The Stacks Project, Tag 04DD, universal homeomorphisms.
• The Stacks Project, Tag 04DF, the integral characterization of universal homeomorphisms.
• The Stacks Project, Tag 01S4, the field-valued criterion for universal injectivity.

theorem AlgebraicGeometry.Surjective.of_universally_isHomeomorph {X Y : Scheme} {f : X ⟶ Y} (hf : (topologically @IsHomeomorph).universally f) : Surjective f

A universal homeomorphism is surjective.

theorem AlgebraicGeometry.UniversallyInjective.of_universally_isHomeomorph {X Y : Scheme} {f : X ⟶ Y} (hf : (topologically @IsHomeomorph).universally f) : UniversallyInjective f

A universal homeomorphism is universally injective.

theorem AlgebraicGeometry.UniversallyClosed.of_universally_isHomeomorph {X Y : Scheme} {f : X ⟶ Y} (hf : (topologically @IsHomeomorph).universally f) : UniversallyClosed f

A universal homeomorphism is universally closed.

theorem AlgebraicGeometry.UniversallyInjective.of_comp_surjective {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [UniversallyInjective (CategoryTheory.CategoryStruct.comp f g)] [Surjective f] : UniversallyInjective g

If f ≫ g is universally injective and f is surjective, then g is universally injective.

class TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

Every base change of a universal homeomorphism is a homeomorphism on underlying spaces.

• universally_isHomeomorph : (AlgebraicGeometry.topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => IsHomeomorph).universally f

theorem TauCeti.AlgebraicGeometry.isUniversalHomeomorphism_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : IsUniversalHomeomorphism f ↔ (AlgebraicGeometry.topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => IsHomeomorph).universally f

theorem TauCeti.AlgebraicGeometry.isUniversalHomeomorphism_eq : @IsUniversalHomeomorphism = (AlgebraicGeometry.topologically fun {α β : Type u} [TopologicalSpace α] [TopologicalSpace β] => IsHomeomorph).universally

Universal homeomorphisms are the universal closure of the homeomorphism property.

instance TauCeti.AlgebraicGeometry.isUniversalHomeomorphism_respectsIso : CategoryTheory.MorphismProperty.RespectsIso @IsUniversalHomeomorphism

instance TauCeti.AlgebraicGeometry.isUniversalHomeomorphism_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsUniversalHomeomorphism

theorem TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.isHomeomorph {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] : IsHomeomorph ⇑f

A universal homeomorphism induces a homeomorphism before any base change.

instance TauCeti.AlgebraicGeometry.instSurjectiveOfIsUniversalHomeomorphism {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] : AlgebraicGeometry.Surjective f

Universal homeomorphisms are surjective on points.

instance TauCeti.AlgebraicGeometry.instUniversallyClosedOfIsUniversalHomeomorphism {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] : AlgebraicGeometry.UniversallyClosed f

Universal homeomorphisms are universally closed.

instance TauCeti.AlgebraicGeometry.instUniversallyInjectiveOfIsUniversalHomeomorphism {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] : AlgebraicGeometry.UniversallyInjective f

Universal homeomorphisms are universally injective.

theorem TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.surjective {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (h : IsUniversalHomeomorphism f) : AlgebraicGeometry.Surjective f

An explicit universal-homeomorphism hypothesis implies surjectivity on points.

theorem TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.universallyClosed {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (h : IsUniversalHomeomorphism f) : AlgebraicGeometry.UniversallyClosed f

An explicit universal-homeomorphism hypothesis implies universal closedness.

theorem TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.universallyInjective {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} (h : IsUniversalHomeomorphism f) : AlgebraicGeometry.UniversallyInjective f

An explicit universal-homeomorphism hypothesis implies universal injectivity.

instance TauCeti.AlgebraicGeometry.instIsUniversalHomeomorphismSndScheme {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsUniversalHomeomorphism f] : IsUniversalHomeomorphism (CategoryTheory.Limits.pullback.snd f g)

The second pullback projection is a universal homeomorphism when the first input map is.

instance TauCeti.AlgebraicGeometry.instIsUniversalHomeomorphismFstScheme {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsUniversalHomeomorphism g] : IsUniversalHomeomorphism (CategoryTheory.Limits.pullback.fst f g)

The first pullback projection is a universal homeomorphism when the second input map is.

theorem TauCeti.AlgebraicGeometry.isUniversalHomeomorphism_iff_universallyClosed_universallyInjective_surjective {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : IsUniversalHomeomorphism f ↔ AlgebraicGeometry.UniversallyClosed f ∧ AlgebraicGeometry.UniversallyInjective f ∧ AlgebraicGeometry.Surjective f

Universally closed, universally injective, surjective scheme maps are precisely the universal homeomorphisms.

instance TauCeti.AlgebraicGeometry.instIsIntegralHomOfIsUniversalHomeomorphism {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] : AlgebraicGeometry.IsIntegralHom f

Universal homeomorphisms are integral.

theorem TauCeti.AlgebraicGeometry.isUniversalHomeomorphism_iff_isIntegralHom_universallyInjective_surjective {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : IsUniversalHomeomorphism f ↔ AlgebraicGeometry.IsIntegralHom f ∧ AlgebraicGeometry.UniversallyInjective f ∧ AlgebraicGeometry.Surjective f

Integral, universally injective, surjective scheme maps are precisely the universal homeomorphisms.

instance TauCeti.AlgebraicGeometry.isUniversalHomeomorphism_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget @IsUniversalHomeomorphism

Being a universal homeomorphism is local on the target.

theorem TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.SpecMap_iff {R S : CommRingCat} (φ : R ⟶ S) : IsUniversalHomeomorphism (AlgebraicGeometry.Spec.map φ) ↔ (CommRingCat.Hom.hom φ).IsIntegral ∧ (∀ (K : Type u) [inst : Field K], Function.Injective fun (g : S ⟶ ↧K) => CategoryTheory.CategoryStruct.comp φ g) ∧ Function.Surjective (PrimeSpectrum.comap (CommRingCat.Hom.hom φ))

Spec.map φ is a universal homeomorphism iff φ is integral, precomposition by φ is injective on maps from S into every field, and PrimeSpectrum.comap φ.hom is surjective.

instance TauCeti.AlgebraicGeometry.isUniversalHomeomorphism_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @IsUniversalHomeomorphism

Composites of universal homeomorphisms are universal homeomorphisms.

instance TauCeti.AlgebraicGeometry.instIsUniversalHomeomorphismCompScheme {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsUniversalHomeomorphism f] [IsUniversalHomeomorphism g] : IsUniversalHomeomorphism (CategoryTheory.CategoryStruct.comp f g)

Typeclass inference recognizes composites of universal homeomorphisms.

instance TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.of_isIso {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : IsUniversalHomeomorphism f

Every isomorphism of schemes is a universal homeomorphism.

noncomputable def TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.homeomorph {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] : ↥X ≃ₜ ↥Y

The homeomorphism of underlying spaces induced by a universal homeomorphism of schemes.

@[simp]

theorem TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.homeomorph_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] (x : ↥X) : (homeomorph f) x = f x

@[simp]

theorem TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.homeomorph_symm_apply_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] (x : ↥X) : (homeomorph f).symm (f x) = x

The inverse underlying homeomorphism sends the image of a point back to that point.

@[simp]

theorem TauCeti.AlgebraicGeometry.IsUniversalHomeomorphism.homeomorph_apply_symm_apply {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsUniversalHomeomorphism f] (y : ↥Y) : f ((homeomorph f).symm y) = y

Mapping the point supplied by the inverse homeomorphism recovers the original point.