Modifications

A morphism of schemes f : X ⟶ Y is a modification if it is proper and there is a dense open U ⊆ Y, with dense preimage f ⁻¹ U ⊆ X, over which f is an isomorphism (Stacks, Definition 29.52.11 (0AAZ), where X and Y are integral). Blow-ups and finite normalizations of integral schemes are typical examples. A modification changes its target only over a nowhere dense closed subset, so it identifies dense opens of source and target: it is birational over its target.

Main definitions

• TauCeti.AlgebraicGeometry.IsModification f: f is proper and an isomorphism over a dense open with dense preimage.

Main results

• TauCeti.AlgebraicGeometry.IsModification.of_isIso: isomorphisms are modifications.
• TauCeti.AlgebraicGeometry.IsModification.birationalOver: a modification f : X ⟶ Y is birational over Y, comparing f with the identity of Y.
• TauCeti.AlgebraicGeometry.IsModification.birational: the source and target of a modification are birational.

References

• Stacks Project, Definition 29.52.11.

class TauCeti.AlgebraicGeometry.IsModification {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.IsProper f : Prop

A morphism of schemes f : X ⟶ Y is a modification if it is proper and there is a dense open U ⊆ Y with dense preimage in X over which f is an isomorphism. Stacks, Definition 29.52.11 (0AAZ), where X and Y are integral.

• isClosedImmersion_diagonal : IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)
• universally_isClosedMap : (topologically @IsClosedMap).universally f
• finiteType_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType
• exists_isIso_morphismRestrict : ∃ (U : Y.Opens), Dense ↑U ∧ Dense ↑((TopologicalSpace.Opens.map f.base).obj U) ∧ CategoryTheory.IsIso (f ∣_ U)

@[instance 100]

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

An isomorphism is a modification, over the whole target.

theorem TauCeti.AlgebraicGeometry.IsModification.birationalOver {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsModification f] : AlgebraicGeometry.Scheme.BirationalOver f (CategoryTheory.CategoryStruct.id Y)

A modification f : X ⟶ Y is birational over Y: restricting f over a dense open of Y gives a partial isomorphism from X to Y lying over Y.

theorem TauCeti.AlgebraicGeometry.IsModification.birational {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [IsModification f] : X.Birational Y

The source and target of a modification are birational.