Scheme-theoretically dominant morphisms

In this file, we define scheme-theoretically dominant morphisms as morphisms with trivial kernel.

Main results

• AlgebraicGeometry.IsSchemeTheoreticallyDominant: The class of scheme-theoretically dominant morphisms.
• AlgebraicGeometry.isSchemeTheoreticallyDominant_iff_isDominant: If the target is reduced and the map is quasi-compact, then scheme-theoretically dominant is equivalent to dominant.
• AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isPullback: quasicompact + scheme-theoretically dominant is stable under flat base change.

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

A morphism is scheme-theoretically dominant if its kernel is trivial.

• ker_eq_bot : Scheme.Hom.ker f = ⊥

theorem AlgebraicGeometry.isSchemeTheoreticallyDominant_iff {X Y : Scheme} (f : X ⟶ Y) : IsSchemeTheoreticallyDominant f ↔ Scheme.Hom.ker f = ⊥

theorem AlgebraicGeometry.Scheme.Hom.ker_eq_bot {X Y : Scheme} (f : X ⟶ Y) [self : IsSchemeTheoreticallyDominant f] : ker f = ⊥

Alias of AlgebraicGeometry.IsSchemeTheoreticallyDominant.ker_eq_bot.

@[instance 100]

instance AlgebraicGeometry.instIsSchemeTheoreticallyDominantOfIsIsoScheme {X S : Scheme} (f : X ⟶ S) [CategoryTheory.IsIso f] : IsSchemeTheoreticallyDominant f

@[instance 100]

instance AlgebraicGeometry.instIsDominantOfIsSchemeTheoreticallyDominantOfQuasiCompact {X S : Scheme} (f : X ⟶ S) [IsSchemeTheoreticallyDominant f] [QuasiCompact f] : IsDominant f

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

instance AlgebraicGeometry.instIsMultiplicativeSchemeIsSchemeTheoreticallyDominant : CategoryTheory.MorphismProperty.IsMultiplicative @IsSchemeTheoreticallyDominant

theorem AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isDominant {X Y : Scheme} (f : X ⟶ Y) [IsDominant f] [IsReduced Y] : IsSchemeTheoreticallyDominant f

theorem AlgebraicGeometry.isSchemeTheoreticallyDominant_iff_isDominant {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] [IsReduced Y] : IsSchemeTheoreticallyDominant f ↔ IsDominant f

If the target is reduced and the map is quasi-compact, then scheme-theoretically dominant is equivalent to dominant.

theorem AlgebraicGeometry.Scheme.Hom.app_injective {X Y : Scheme} (f : X ⟶ Y) [IsSchemeTheoreticallyDominant f] [QuasiCompact f] (U : Y.Opens) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (app f U))

theorem AlgebraicGeometry.IsSchemeTheoreticallyDominant.isReduced {X Y : Scheme} (f : X ⟶ Y) [IsSchemeTheoreticallyDominant f] [QuasiCompact f] [IsReduced X] : IsReduced Y

instance AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackSnd {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsSchemeTheoreticallyDominant f] [QuasiCompact f] [Flat g] : IsSchemeTheoreticallyDominant (CategoryTheory.Limits.pullback.snd f g)

theorem AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isPullback {X Y Z S : Scheme} {f : X ⟶ S} {g : Y ⟶ S} {pX : Z ⟶ X} {pY : Z ⟶ Y} (H : CategoryTheory.IsPullback pX pY f g) [IsSchemeTheoreticallyDominant f] [QuasiCompact f] [Flat g] : IsSchemeTheoreticallyDominant pY

instance AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackFst {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsSchemeTheoreticallyDominant g] [QuasiCompact g] [Flat f] : IsSchemeTheoreticallyDominant (CategoryTheory.Limits.pullback.fst f g)