# Documentation

Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

# Properties of morphisms from properties of ring homs. #

We provide the basic framework for talking about properties of morphisms that come from properties of ring homs. For P a property of ring homs, we have two ways of defining a property of scheme morphisms:

Let f : X ⟶ Y,

• targetAffineLocally (affine_and P): the preimage of an affine open U = Spec A is affine (= Spec B) and A ⟶ B satisfies P. (TODO)
• affineLocally P: For each pair of affine open U = Spec A ⊆ X and V = Spec B ⊆ f ⁻¹' U, the ring hom A ⟶ B satisfies P.

For these notions to be well defined, we require P be a sufficient local property. For the former, P should be local on the source (RingHom.RespectsIso P, RingHom.LocalizationPreserves P, RingHom.OfLocalizationSpan), and targetAffineLocally (affine_and P) will be local on the target. (TODO)

For the latter P should be local on the target (RingHom.PropertyIsLocal P), and affineLocally P will be local on both the source and the target.

Further more, these properties are stable under compositions (resp. base change) if P is. (TODO)

theorem RingHom.RespectsIso.basicOpen_iff_localization {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) (r : ↑(Y.presheaf.obj ())) :
theorem RingHom.RespectsIso.ofRestrict_morphismRestrict_iff {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) (r : ↑(Y.presheaf.obj ())) (U : TopologicalSpace.Opens X.toPresheafedSpace) (hU : ) {V : TopologicalSpace.Opens (AlgebraicGeometry.Scheme.restrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj ())))).toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace} (e : V = (TopologicalSpace.Opens.map (AlgebraicGeometry.Scheme.ofRestrict X (_ : OpenEmbedding ↑(TopologicalSpace.Opens.inclusion ((TopologicalSpace.Opens.map f.val.base).obj ())))).val.base).obj U) :
theorem RingHom.StableUnderBaseChange.Γ_pullback_fst {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (hP' : ) (f : X S) (g : Y S) (H : P (↑()) (↑()) () () (AlgebraicGeometry.Scheme.Γ.map g.op)) :
P (↑()) (↑()) () () (AlgebraicGeometry.Scheme.Γ.map CategoryTheory.Limits.pullback.fst.op)
def AlgebraicGeometry.sourceAffineLocally (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

For P a property of ring homomorphisms, sourceAffineLocally P holds for f : X ⟶ Y whenever P holds for the restriction of f on every affine open subset of X.

Instances For
@[inline, reducible]
abbrev AlgebraicGeometry.affineLocally (P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop) :

For P a property of ring homomorphisms, affineLocally P holds for f : X ⟶ Y if for each affine open U = Spec A ⊆ Y and V = Spec B ⊆ f ⁻¹' U, the ring hom A ⟶ B satisfies P. Also see affineLocally_iff_affineOpens_le.

Instances For
theorem AlgebraicGeometry.sourceAffineLocally_respectsIso {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (h₁ : ) :
theorem AlgebraicGeometry.affineLocally_respectsIso {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (h : ) :
theorem AlgebraicGeometry.affineLocally_iff_affineOpens_le {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) :
(U : ) → (V : ) → (e : V (TopologicalSpace.Opens.map f.val.base).obj U) → P (↑(Y.presheaf.obj ())) (↑(X.presheaf.obj ())) (CommRingCat.instCommRingα (Y.presheaf.obj ())) (CommRingCat.instCommRingα (X.presheaf.obj ())) ()
theorem AlgebraicGeometry.sourceAffineLocally_isLocal {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (h₁ : ) (h₂ : ) (h₃ : ) :
theorem AlgebraicGeometry.sourceAffineLocally_of_source_open_cover_aux {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (h₁ : ) (h₃ : ) (f : X Y) (U : ) (s : Set ↑(X.presheaf.obj ())) (hs : ) (hs' : (r : s) → P (↑()) (↑(AlgebraicGeometry.Scheme.Γ.obj (Opposite.op ()))) () (CommRingCat.instCommRingα (AlgebraicGeometry.Scheme.Γ.obj (Opposite.op ()))) (AlgebraicGeometry.Scheme.Γ.map ().op)) :
P (↑()) (↑(AlgebraicGeometry.Scheme.Γ.obj ())) () () (AlgebraicGeometry.Scheme.Γ.map ().op)
theorem AlgebraicGeometry.isOpenImmersionCat_comp_of_sourceAffineLocally {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (h₁ : ) (f : X Y) (g : Y Z) (h₂ : ) :
P (↑()) (↑()) () () ()
theorem RingHom.PropertyIsLocal.sourceAffineLocally_of_source_openCover {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) [∀ (i : 𝒰.J), ] (H : (i : 𝒰.J) → P (↑()) () () () ()) :
theorem RingHom.PropertyIsLocal.affine_openCover_TFAE {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) :
List.TFAE [, 𝒰 x, (i : 𝒰.J) → P (↑()) () () () (), (𝒰 : ) → [inst : ∀ (i : 𝒰.J), ] → (i : 𝒰.J) → P (↑()) () () () (), {U : AlgebraicGeometry.Scheme} → (g : U X) → [inst : ] → [inst : ] → P (↑()) (↑()) () () ()]
theorem RingHom.PropertyIsLocal.openCover_TFAE {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) :
List.TFAE [, 𝒰, ∀ (i : 𝒰.J), , ∀ (𝒰 : ) (i : 𝒰.J), , ∀ {U : AlgebraicGeometry.Scheme} (g : U X) [inst : ], ]
theorem RingHom.PropertyIsLocal.sourceAffineLocally_comp_of_isOpenImmersion {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) (g : Y Z) :
theorem RingHom.PropertyIsLocal.source_affine_openCover_iff {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) [∀ (i : 𝒰.J), ] :
(i : 𝒰.J) → P (↑()) () () () ()
theorem RingHom.PropertyIsLocal.isLocal_sourceAffineLocally {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) :
theorem RingHom.PropertyIsLocal.is_local_affineLocally {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) :
theorem RingHom.PropertyIsLocal.affine_openCover_iff {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) [∀ (i : 𝒰.J), ] [∀ (i : ) (j : (𝒰' i).J), ] :
(i : ) → (j : (𝒰' i).J) → P () (↑(AlgebraicGeometry.Scheme.Γ.obj ())) () () (AlgebraicGeometry.Scheme.Γ.map (CategoryTheory.CategoryStruct.comp () CategoryTheory.Limits.pullback.snd).op)
theorem RingHom.PropertyIsLocal.source_openCover_iff {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) :
(i : 𝒰.J) →
theorem RingHom.PropertyIsLocal.affineLocally_of_isOpenImmersion {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (f : X Y) :
theorem RingHom.PropertyIsLocal.affineLocally_of_comp {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) (H : {R S T : Type u} → [inst : ] → [inst_1 : ] → [inst_2 : ] → (f : R →+* S) → (g : S →+* T) → P R T inst inst_2 ()P S T inst_1 inst_2 g) {f : X Y} {g : Y Z} :
theorem RingHom.PropertyIsLocal.affineLocally_stableUnderComposition {P : {R S : Type u} → [inst : ] → [inst_1 : ] → (R →+* S) → Prop} (hP : ) :