Geometrically integral morphisms #
Mathlib's AlgebraicGeometry.GeometricallyIntegral records that the property is stable under base
change, but has nothing about isomorphisms. This file adds the missing base case:
AlgebraicGeometry.geometricallyIntegral_of_isIso: an isomorphism of schemes is geometrically integral.
No external mathematics is vendored; the proof reuses Mathlib's stability of the isomorphism morphism property under pullback and the integrality of a scheme isomorphic to an integral one.
theorem
TauCeti.AlgebraicGeometry.geometricallyIntegral_of_isIso
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
:
An isomorphism of schemes is geometrically integral.
Every base change of an isomorphism is an isomorphism, so the fibre product of f with a morphism
Spec L ⟶ Y is isomorphic to Spec L, which is integral because L is a field.