Geometrically connected schemes

In this file we define geometrically connected morphisms of schemes. A morphism f : X ⟶ Y is geometrically connected if for all Spec K ⟶ Y with K a field, X ×[Y] Spec K is connected. In the case where Y = Spec K for some field K this recovers the standard definition of a geometrically connected scheme over a field.

Main results

• AlgebraicGeometry.GeometricallyConnected: A morphism f : X ⟶ Y is geometrically connected if for all Spec K ⟶ Y with K a field, X ×[Y] Spec K is connected.
• GeometricallyConnected.iff_geometricallyConnected_fiber: A scheme is geometrically connected over S iff the fibers of all s : S are geometrically connected.

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

We say that a morphism f : X ⟶ Y is geometrically connected if for all Spec K ⟶ Y with K a field, X ×[Y] Spec K is connected.

• geometrically_connectedSpace : geometrically (fun (x : Scheme) => ConnectedSpace ↥x) f

theorem AlgebraicGeometry.geometricallyConnected_iff {X Y : Scheme} (f : X ⟶ Y) : GeometricallyConnected f ↔ geometrically (fun (x : Scheme) => ConnectedSpace ↥x) f

theorem AlgebraicGeometry.GeometricallyConnected.eq_geometrically : @GeometricallyConnected = geometrically fun (x : Scheme) => ConnectedSpace ↥x

instance AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyConnected : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @GeometricallyConnected

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

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

instance AlgebraicGeometry.instGeometricallyConnectedMorphismRestrict {X S : Scheme} (f : X ⟶ S) (V : S.Opens) [GeometricallyConnected f] : GeometricallyConnected (f ∣_ V)

instance AlgebraicGeometry.instGeometricallyConnectedFiberToSpecResidueField {X S : Scheme} (f : X ⟶ S) (s : ↥S) [GeometricallyConnected f] : GeometricallyConnected (Scheme.Hom.fiberToSpecResidueField f s)

instance AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatFiberOfGeometricallyConnected {X S : Scheme} (f : X ⟶ S) (s : ↥S) [GeometricallyConnected f] : ConnectedSpace ↥(Scheme.Hom.fiber f s)

@[instance 100]

instance AlgebraicGeometry.instSurjectiveOfGeometricallyConnected {X S : Scheme} (f : X ⟶ S) [GeometricallyConnected f] : Surjective f

theorem AlgebraicGeometry.Scheme.Hom.isConnected_preimage_singleton {X S : Scheme} (f : X ⟶ S) [GeometricallyConnected f] (x : ↥S) : IsConnected (⇑f ⁻¹' {x})

theorem AlgebraicGeometry.Scheme.Hom.isConnected_preimage {X S : Scheme} (f : X ⟶ S) [GeometricallyConnected f] (hf : IsOpenMap ⇑f) {s : Set ↥S} (hs : IsConnected s) (hs' : IsClosed s) : IsConnected (⇑f ⁻¹' s)

noncomputable def AlgebraicGeometry.Scheme.Hom.connectedComponentsHomeomorph {X S : Scheme} (f : X ⟶ S) [GeometricallyConnected f] (hf : IsOpenMap ⇑f) : ConnectedComponents ↥X ≃ₜ ConnectedComponents ↥S

If f : X ⟶ S is geometrically connected and open, then f induces a homeomorphism between the connected components of X and S.

Equations

• AlgebraicGeometry.Scheme.Hom.connectedComponentsHomeomorph f hf = ⋯.connectedComponentsHomeomorph ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.connectedComponentsHomeomorph_apply {X S : Scheme} (f : X ⟶ S) [GeometricallyConnected f] (hf : IsOpenMap ⇑f) (a✝ : ConnectedComponents ↥X) : (connectedComponentsHomeomorph f hf) a✝ = ⋯.connectedComponentsMap a✝

theorem AlgebraicGeometry.GeometricallyConnected.connectedSpace {X S : Scheme} (f : X ⟶ S) [GeometricallyConnected f] [ConnectedSpace ↥S] (hf : IsOpenMap ⇑f) : ConnectedSpace ↥X

theorem AlgebraicGeometry.GeometricallyConnected.connectedSpace_of_subsingleton {X S : Scheme} (f : X ⟶ S) [GeometricallyConnected f] [Subsingleton ↥S] [Nonempty ↥S] : ConnectedSpace ↥X

If X is geometrically connected over a point, then it is connected.

instance AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyConnectedOfUniversallyOpen {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyConnected f] [UniversallyOpen f] [ConnectedSpace ↥Y] : ConnectedSpace ↥(CategoryTheory.Limits.pullback f g)

instance AlgebraicGeometry.instConnectedSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyConnectedOfUniversallyOpen_1 {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyConnected g] [UniversallyOpen g] [ConnectedSpace ↥X] : ConnectedSpace ↥(CategoryTheory.Limits.pullback f g)

theorem AlgebraicGeometry.GeometricallyConnected.iff_geometricallyConnected_fiber {X S : Scheme} (f : X ⟶ S) : GeometricallyConnected f ↔ ∀ (s : ↥S), GeometricallyConnected (Scheme.Hom.fiberToSpecResidueField f s)

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