ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>S : Finset R<VAR>hS : Ideal.span ↑S = ⊤<VAR>hN : ∀ (s : { x // x ∈ S }), IsNoetherianRing (Localization.Away ↑s)<GOAL>IsNoetherianRing R
<VAR>X : AlgebraicGeometry.Scheme<VAR>ι : Sort u_1<VAR>S : ι → ↑X.affineOpens<VAR>hS : ⨆ i, ↑(S i) = ⊤<VAR>hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))<GOAL>AlgebraicGeometry.IsLocallyNoetherian X
<VAR>X : AlgebraicGeometry.Scheme<VAR>ι : Sort u_1<VAR>S : ι → ↑X.affineOpens<VAR>hS : ⨆ i, ↑(S i) = ⊤<GOAL>AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)<GOAL>AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion f<VAR>AlgebraicGeometry.IsLocallyNoetherian Y<GOAL>AlgebraicGeometry.IsLocallyNoetherian X
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<GOAL>AlgebraicGeometry.IsLocallyNoetherian X ↔ ∀ (i : 𝒰.J), AlgebraicGeometry.IsLocallyNoetherian (𝒰.obj i)
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine X<VAR>IsNoetherianRing ↑Γ(X, ⊤)<GOAL>TopologicalSpace.NoetherianSpace ↑↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>IsNoetherianRing ↑Γ(X, U)<GOAL>TopologicalSpace.NoetherianSpace ↑↑(↑U).toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<GOAL>AlgebraicGeometry.IsNoetherian X ↔ AlgebraicGeometry.IsLocallyNoetherian X ∧ CompactSpace ↑↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<VAR>ι : Sort u_1<VAR>Finite ι<VAR>S : ι → ↑X.affineOpens<VAR>hS : ⨆ i, ↑(S i) = ⊤<GOAL>AlgebraicGeometry.IsNoetherian X ↔ ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
<VAR>X : AlgebraicGeometry.Scheme<VAR>𝒰 : X.OpenCover<VAR>Finite 𝒰.J<VAR>∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)<GOAL>AlgebraicGeometry.IsNoetherian X ↔ ∀ (i : 𝒰.J), IsNoetherianRing ↑Γ(𝒰.obj i, ⊤)
<VAR>R : CommRingCat<GOAL>AlgebraicGeometry.IsNoetherian (AlgebraicGeometry.Spec R) ↔ IsNoetherianRing ↑R
<VAR>X : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsNoetherian X<GOAL>(irreducibleComponents ↑↑X.toPresheafedSpace).Finite
<VAR>R : Type u<VAR>CommRing R<VAR>IsNoetherianRing R<GOAL>(minimalPrimes R).Finite
<VAR>R : Type u<VAR>CommRing R<GOAL>Set.range MaximalSpectrum.toPrimeSpectrum = {x | IsClosed {x}}
<VAR>R : Type u<VAR>CommRing R<GOAL>Continuous MaximalSpectrum.toPrimeSpectrum
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : (x : ↥U) → ModuleCat.Tilde.Localizations M ↑x<GOAL>(ModuleCat.Tilde.isLocallyFraction M).pred f = ∀ (y : ↥U), ∃ V, ∃ (_ : ↑y ∈ V), ∃ i m s, ∀ (x : ↥V), s ∉ (↑x).asIdeal ∧ s • f ((fun x => ⟨↑x, ⋯⟩) x) = (LocalizedModule.mkLinearMap (↑x).asIdeal.primeCompl ↑M) m
<VAR>R : Type u<VAR>CommRing R<VAR>M : ModuleCat R<VAR>U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ<VAR>x : ↥(Opposite.unop U)<VAR>r : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj U)<VAR>m : ModuleCat.Tilde.Localizations M ↑x<GOAL>r • m = ↑r x • m
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>f : R<GOAL>Subsingleton (LocalizedModule (Submonoid.powers f) M) ↔ Disjoint (↑(PrimeSpectrum.basicOpen f)) (Module.support R M)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<GOAL>StableUnderSpecialization (Module.support R M)
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>Module.Finite R M<GOAL>IsClosed (Module.support R M)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>CommRing R<VAR>AddCommGroup M<VAR>Module R M<VAR>CommRing A<VAR>Algebra R A<VAR>Module A M<VAR>IsScalarTower R A M<GOAL>Module.support A M ⊆ ⇑(PrimeSpectrum.comap (algebraMap R A)) ⁻¹' Module.support R M
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R[X]<GOAL>IsOpen (AlgebraicGeometry.Polynomial.imageOfDf f)
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R[X]<VAR>I : PrimeSpectrum R[X]<VAR>H : I ∈ (PrimeSpectrum.zeroLocus {f})ᶜ<GOAL>(PrimeSpectrum.comap Polynomial.C) I ∈ AlgebraicGeometry.Polynomial.imageOfDf f
<VAR>R : Type u_1<VAR>CommRing R<VAR>f : R[X]<GOAL>AlgebraicGeometry.Polynomial.imageOfDf f = ⇑(PrimeSpectrum.comap Polynomial.C) '' (PrimeSpectrum.zeroLocus {f})ᶜ
<VAR>R : Type u_1<VAR>CommRing R<GOAL>IsOpenMap ⇑(PrimeSpectrum.comap Polynomial.C)
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i : D.J<GOAL>D.oneHypercover.f i = D.ι i
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i₁ i₂ : D.J<GOAL>∀ (x : PUnit.{u + 1}), D.oneHypercover.p₁ x = D.f i₁ i₂
<VAR>D : AlgebraicGeometry.Scheme.GlueData<GOAL>∀ (a : D.J), D.oneHypercover.X a = D.U a
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i₁ i₂ : D.J<GOAL>∀ (x : PUnit.{u + 1}), D.oneHypercover.Y x = D.V (i₁, i₂)
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>i₁ i₂ : D.J<VAR>j : PUnit.{u + 1}<GOAL>D.oneHypercover.p₂ j = D.t i₁ i₂ ≫ D.f i₂ i₁
<VAR>D : AlgebraicGeometry.Scheme.GlueData<GOAL>D.oneHypercover.I₀ = D.J
<VAR>D : AlgebraicGeometry.Scheme.GlueData<GOAL>∀ (x x_1 : D.J), D.oneHypercover.I₁ x x_1 = PUnit.{u + 1}
<VAR>D : AlgebraicGeometry.Scheme.GlueData<VAR>F : CategoryTheory.Sheaf AlgebraicGeometry.Scheme.zariskiTopology (Type v)<VAR>s : (j : D.J) → F.val.obj (Opposite.op (D.U j))<VAR>h : ∀ (i j : D.J), F.val.map (D.f i j).op (s i) = F.val.map ((D.f j i).op ≫ (D.t i j).op) (s j)<VAR>j : D.J<GOAL>F.val.map (D.ι j).op (D.sheafValGluedMk s h) = s j
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsLocalAtTarget P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<GOAL>P f ↔ ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsLocalAtTarget P<GOAL>P.RespectsIso
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>P.RespectsIso<VAR>restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : Y.Opens), P f → P (f ∣_ U)<VAR>of_sSup_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f<GOAL>AlgebraicGeometry.IsLocalAtTarget P
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>hP : AlgebraicGeometry.IsLocalAtTarget P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>UX UY : AlgebraicGeometry.Scheme<VAR>iY : UY ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion iY<VAR>iX : UX ⟶ X<VAR>f' : UX ⟶ UY<VAR>h : CategoryTheory.IsPullback iX f' f iY<VAR>H : P f<GOAL>P f'
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>hP : AlgebraicGeometry.IsLocalAtTarget P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>hf : P f<VAR>U : Y.Opens<GOAL>P (f ∣_ U)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>hP : AlgebraicGeometry.IsLocalAtTarget P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P (f ∣_ U i)<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>hP : AlgebraicGeometry.IsLocalAtTarget P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → Y.Opens<VAR>hU : iSup U = ⊤<GOAL>P f ↔ ∀ (i : ι), P (f ∣_ U i)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>hP : AlgebraicGeometry.IsLocalAtTarget P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>H : ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>hP : AlgebraicGeometry.IsLocalAtTarget P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<GOAL>P f ↔ ∀ (i : (𝒰.pullbackCover f).J), P (𝒰.pullbackHom f i)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsLocalAtSource P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<GOAL>P f ↔ ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsLocalAtSource P<GOAL>P.RespectsIso
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>P.RespectsIso<VAR>restrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : X.Opens), P f → P (U.ι ≫ f)<VAR>of_sSup_eq_top : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → X.Opens), iSup U = ⊤ → (∀ (i : ι), P ((U i).ι ≫ f)) → P f<GOAL>AlgebraicGeometry.IsLocalAtSource P
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtSource P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>UX : AlgebraicGeometry.Scheme<VAR>H : P f<VAR>i : UX ⟶ X<VAR>AlgebraicGeometry.IsOpenImmersion i<GOAL>P (i ≫ f)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtSource P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → X.Opens<VAR>hU : iSup U = ⊤<VAR>H : ∀ (i : ι), P ((U i).ι ≫ f)<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtSource P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → X.Opens<VAR>hU : iSup U = ⊤<GOAL>P f ↔ ∀ (i : ι), P ((U i).ι ≫ f)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtSource P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<VAR>H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtSource P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : X.OpenCover<GOAL>P f ↔ ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtSource P<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>P.ContainsIdentities<VAR>AlgebraicGeometry.IsOpenImmersion f<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtSource P<VAR>P.IsMultiplicative<VAR>hP : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [inst : AlgebraicGeometry.IsOpenImmersion g], P (f ≫ g) → P f<GOAL>AlgebraicGeometry.IsLocalAtTarget P
<VAR>P Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>H : ∀ ⦃X Y : AlgebraicGeometry.Scheme⦄ (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffine Y], P f ↔ Q f<GOAL>P = Q
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>i : AlgebraicGeometry.IsAffine Y<GOAL>P.toProperty f ↔ P f
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>P.toProperty.RespectsIso<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso f<VAR>AlgebraicGeometry.IsAffine Z<GOAL>P (f ≫ g) ↔ P g
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>P.toProperty.RespectsIso<VAR>X Y Z : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>CategoryTheory.IsIso g<VAR>AlgebraicGeometry.IsAffine Z<VAR>AlgebraicGeometry.IsAffine Y<GOAL>P (f ≫ g) ↔ P f
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>P.toProperty.RespectsIso<VAR>X Y X' Y' : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>f' : X' ⟶ Y'<VAR>e : CategoryTheory.Arrow.mk f ≅ CategoryTheory.Arrow.mk f'<VAR>h : AlgebraicGeometry.IsAffine Y<GOAL>P f ↔ P f'
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>h₁ : ∀ {X Y Z : AlgebraicGeometry.Scheme} (e : X ≅ Y) (f : Y ⟶ Z) [inst : AlgebraicGeometry.IsAffine Z], P f → P (e.hom ≫ f)<VAR>h₂ : ∀ {X Y Z : AlgebraicGeometry.Scheme} (e : Y ≅ Z) (f : X ⟶ Y) [h : AlgebraicGeometry.IsAffine Y], P f → P (f ≫ e.hom)<GOAL>P.toProperty.RespectsIso
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>self : P.IsLocal<VAR>X Y : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine Y<VAR>f : X ⟶ Y<VAR>r : ↑(Y.presheaf.obj (Opposite.op ⊤))<GOAL>P f → P (f ∣_ Y.basicOpen r)
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>self : P.IsLocal<VAR>X Y : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine Y<VAR>f : X ⟶ Y<VAR>s : Finset ↑(Y.presheaf.obj (Opposite.op ⊤))<GOAL>Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (f ∣_ Y.basicOpen ↑r)) → P f
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>self : P.IsLocal<GOAL>P.toProperty.RespectsIso
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>P.toProperty.RespectsIso<VAR>H : ∀ ⦃X Y S : AlgebraicGeometry.Scheme⦄ [inst : AlgebraicGeometry.IsAffine S] [inst_1 : AlgebraicGeometry.IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), P g → P (CategoryTheory.Limits.pullback.fst f g)<GOAL>P.StableUnderBaseChange
<VAR>P : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>P.IsLocal<VAR>X Y UX UY : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine UY<VAR>f : X ⟶ Y<VAR>iY : UY ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion iY<VAR>iX : UX ⟶ X<VAR>f' : UX ⟶ UY<VAR>h : CategoryTheory.IsPullback iX f' f iY<VAR>hf : AlgebraicGeometry.targetAffineLocally P f<GOAL>P f'
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : outParam AlgebraicGeometry.AffineTargetMorphismProperty<VAR>self : AlgebraicGeometry.HasAffineProperty P Q<GOAL>P = AlgebraicGeometry.targetAffineLocally Q
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : outParam AlgebraicGeometry.AffineTargetMorphismProperty<VAR>self : AlgebraicGeometry.HasAffineProperty P Q<GOAL>AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal Q
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<GOAL>P = AlgebraicGeometry.targetAffineLocally Q
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtTarget P<GOAL>AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.AffineTargetMorphismProperty.of P)
<VAR>P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q Q' : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>e : P = P'<VAR>e' : Q = Q'<GOAL>AlgebraicGeometry.HasAffineProperty P' Q'
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>UX UY : AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsAffine UY<VAR>iY : UY ⟶ Y<VAR>AlgebraicGeometry.IsOpenImmersion iY<VAR>iX : UX ⟶ X<VAR>f' : UX ⟶ UY<VAR>h : CategoryTheory.IsPullback iX f' f iY<VAR>hf : P f<GOAL>Q f'
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>hf : P f<VAR>U : ↑Y.affineOpens<GOAL>Q (f ∣_ ↑U)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → ↑Y.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<VAR>hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>ι : Sort u_1<VAR>U : ι → ↑Y.affineOpens<VAR>hU : ⨆ i, ↑(U i) = ⊤<GOAL>P f ↔ ∀ (i : ι), Q (f ∣_ ↑(U i))
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)<VAR>h𝒰 : ∀ (i : (𝒰.pullbackCover f).J), Q (𝒰.pullbackHom f i)<GOAL>P f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)<GOAL>P f ↔ ∀ (i : (𝒰.pullbackCover f).J), Q (𝒰.pullbackHom f i)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine Y<GOAL>P f ↔ Q f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<GOAL>AlgebraicGeometry.HasAffineProperty P Q ↔ AlgebraicGeometry.IsLocalAtTarget P ∧ Q = AlgebraicGeometry.AffineTargetMorphismProperty.of P
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>hP' : Q.StableUnderBaseChange<VAR>X Y S : AlgebraicGeometry.Scheme<VAR>f : X ⟶ S<VAR>g : Y ⟶ S<VAR>AlgebraicGeometry.IsAffine S<VAR>H : Q g<GOAL>P (CategoryTheory.Limits.pullback.fst f g)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>hP' : Q.StableUnderBaseChange<GOAL>P.StableUnderBaseChange
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>H : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsAffine Y] (𝒰 : X.OpenCover), Q f ↔ ∀ (i : 𝒰.J), Q (𝒰.map i ≫ f)<GOAL>AlgebraicGeometry.IsLocalAtSource P
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>self : AlgebraicGeometry.IsAffineHom f<VAR>U : Y.Opens<GOAL>AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.val.base).obj U)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<GOAL>AlgebraicGeometry.IsAffineHom f ↔ ∀ (U : Y.Opens), AlgebraicGeometry.IsAffineOpen U → AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.val.base).obj U)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>U : Y.Opens<VAR>hU : AlgebraicGeometry.IsAffineOpen U<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffineHom f<GOAL>AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.val.base).obj U)
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffineHom f<VAR>U : ↑Y.affineOpens<GOAL>↑(AlgebraicGeometry.affinePreimage f U) = (TopologicalSpace.Opens.map f.val.base).obj ↑U
<VAR>X : AlgebraicGeometry.Scheme<VAR>s : Set ↑(X.presheaf.obj (Opposite.op ⊤))<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)<GOAL>QuasiSeparatedSpace ↑↑X.toPresheafedSpace
<VAR>X : AlgebraicGeometry.Scheme<VAR>s : Set ↑(X.presheaf.obj (Opposite.op ⊤))<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)<GOAL>AlgebraicGeometry.IsAffine X
<VAR>X : AlgebraicGeometry.Scheme<VAR>U : X.Opens<VAR>s : Set ↑(X.presheaf.obj (Opposite.op U))<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, AlgebraicGeometry.IsAffineOpen (X.basicOpen i)<GOAL>AlgebraicGeometry.IsAffineOpen U
<GOAL>CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.IsAffineHom
<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffineHom f<VAR>AlgebraicGeometry.IsAffine Y<GOAL>AlgebraicGeometry.IsAffine X
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)<VAR>𝒰' : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover<VAR>∀ (i : 𝒰.J) (j : (𝒰' i).J), AlgebraicGeometry.IsAffine ((𝒰' i).obj j)<VAR>h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (CategoryTheory.Limits.pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (𝒰.pullbackHom f i))<GOAL>P.diagonal f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>𝒰 : Y.OpenCover<VAR>∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)<VAR>h𝒰 : ∀ (i : (𝒰.pullbackCover f).J), Q.diagonal (𝒰.pullbackHom f i)<GOAL>P.diagonal f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y U V : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>AlgebraicGeometry.IsAffine U<VAR>AlgebraicGeometry.IsOpenImmersion g<VAR>iV : V ⟶ X<VAR>f' : V ⟶ U<VAR>h : CategoryTheory.IsPullback iV f' f g<VAR>H : P.diagonal f<GOAL>Q.diagonal f'
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>Q : AlgebraicGeometry.AffineTargetMorphismProperty<VAR>AlgebraicGeometry.HasAffineProperty P Q<VAR>X Y : AlgebraicGeometry.Scheme<VAR>f : X ⟶ Y<VAR>AlgebraicGeometry.IsAffine Y<GOAL>Q.diagonal f ↔ P.diagonal f
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>hP₂ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {ι : Type u} (U : ι → Y.Opens), iSup U = ⊤ → (∀ (i : ι), P (f ∣_ U i)) → P f<GOAL>AlgebraicGeometry.IsLocalAtTarget P.universally
<VAR>P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop<VAR>hP : ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β) (g : β → γ), P f → P g → P (g ∘ f)<GOAL>(AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).IsStableUnderComposition
<VAR>P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop<VAR>hP : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f<GOAL>CategoryTheory.MorphismProperty.isomorphisms AlgebraicGeometry.Scheme ≤ AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P
<VAR>P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop<VAR>hP₁ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f<VAR>hP₂ : ∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α → β) (g : β → γ), P f → P g → P (g ∘ f)<GOAL>(AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso
<VAR>P : {α β : Type u} → [inst : TopologicalSpace α] → [inst : TopologicalSpace β] → (α → β) → Prop<VAR>(AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso<VAR>hP₂ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) (s : Set β), P f → P (s.restrictPreimage f)<VAR>hP₃ : ∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α → β) {ι : Type u} (U : ι → TopologicalSpace.Opens β), iSup U = ⊤ → Continuous f → (∀ (i : ι), P ((U i).carrier.restrictPreimage f)) → P f<GOAL>AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P)
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<GOAL>(AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P).RespectsIso
<VAR>P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P<GOAL>AlgebraicGeometry.IsLocalAtTarget (AlgebraicGeometry.stalkwise fun {R S} [CommRing R] [CommRing S] => P)
<VAR>P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme<VAR>AlgebraicGeometry.IsLocalAtTarget P<VAR>hP₂ : (AlgebraicGeometry.AffineTargetMorphismProperty.of P).StableUnderBaseChange<GOAL>P.StableUnderBaseChange
<VAR>X : AlgebraicGeometry.Scheme<VAR>self : AlgebraicGeometry.IsReduced X<VAR>U : X.Opens<GOAL>IsReduced ↑(X.presheaf.obj (Opposite.op U))
<VAR>X : AlgebraicGeometry.Scheme<VAR>∀ (x : ↑↑X.toPresheafedSpace), IsReduced ↑(X.presheaf.stalk x)<GOAL>AlgebraicGeometry.IsReduced X