AlgebraicGeometry.PropertyIsLocalAtTarget.restrict
theorem AlgebraicGeometry.PropertyIsLocalAtTarget.restrict :
∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
AlgebraicGeometry.PropertyIsLocalAtTarget P →
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (U : TopologicalSpace.Opens ↑↑Y.toPresheafedSpace),
P f → P (f ∣_ U)
This theorem states that if a property `P`, which is a characterization of morphisms between Algebraic Geometry Schemes, holds for a morphism `f` from `X` to `Y`, then the same property `P` also holds for the restriction of `f` to any open set `U` of the topological space of `Y`. Here, the restriction of `f` to `U` is denoted by `f ∣_ U`. So in essence, if a morphism property is local at the target, it remains valid when we restrict our attention to any open set in the target space.
More concisely: If `P` is a property of morphisms between algebraic geometry schemes that holds for `f` from `X` to `Y`, then `P` also holds for the restriction of `f` to any open set `U` of `Y`.
|
AlgebraicGeometry.PropertyIsLocalAtTarget.of_openCover
theorem AlgebraicGeometry.PropertyIsLocalAtTarget.of_openCover :
∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
AlgebraicGeometry.PropertyIsLocalAtTarget P →
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover),
(∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd) → P f
The theorem `AlgebraicGeometry.PropertyIsLocalAtTarget.of_openCover` asserts that if a certain property `P`, which is a class of morphisms between objects in an algebraic geometry scheme, holds for the pullback of a morphism `f` along each open cover `U` of the target `Y`, then the same property `P` holds for the morphism `f` itself. This theorem can be seen as a locality property for morphisms, stating that if something is true in all smaller, local pieces (i.e., the open cover), it is also true in the whole (i.e., the morphism `f`).
More concisely: If a property `P` holds for the pullback of a morphism `f` along each open cover of the target `Y`, then the property `P` holds for the morphism `f`.
|
AlgebraicGeometry.PropertyIsLocalAtTarget.RespectsIso
theorem AlgebraicGeometry.PropertyIsLocalAtTarget.RespectsIso :
∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
AlgebraicGeometry.PropertyIsLocalAtTarget P → P.RespectsIso
The theorem `AlgebraicGeometry.PropertyIsLocalAtTarget.RespectsIso` states that for any `MorphismProperty` `P` in the category of Algebraic Geometry Schemes, if `P` is local at the target, then `P` respects isomorphisms. In other words, if a property `P` holds locally at the target of morphisms in the category of Algebraic Geometry Schemes, then this property `P` is preserved under isomorphisms.
More concisely: If `P` is a morphism property in Algebraic Geometry Schemes that is local at the target, then `P` is preserved under isomorphisms.
|
AlgebraicGeometry.targetAffineLocally_respectsIso
theorem AlgebraicGeometry.targetAffineLocally_respectsIso :
∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
P.toProperty.RespectsIso → (AlgebraicGeometry.targetAffineLocally P).RespectsIso
The theorem `AlgebraicGeometry.targetAffineLocally_respectsIso` states that for any property `P` which classifies morphisms from an arbitrary scheme into an affine scheme, if this property respects isomorphisms when extended to a `MorphismProperty` such that it never holds when the target is not affine, then this property will also respect isomorphisms after being extended to hold whenever `P` holds for the restriction of the morphisms on every affine open subset of the target scheme. In other words, this theorem shows that if a property of morphisms to affine targets respects the composition with isomorphisms, it will continue to respect isomorphisms when considered locally on the target.
More concisely: If a property of morphisms from a scheme to an affine scheme respects isomorphisms and holds for the restriction of morphisms on every affine open subset of the target scheme, then it also respects isomorphisms on the entire target scheme.
|
AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_iff
theorem AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_iff :
∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme},
AlgebraicGeometry.PropertyIsLocalAtTarget P →
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover),
P f ↔ ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd
The theorem `AlgebraicGeometry.PropertyIsLocalAtTarget.openCover_iff` states that for any morphism property `P` in the category of algebraic schemes, if `P` is local at the target, then for any two algebraic schemes `X` and `Y` and any morphism `f` from `X` to `Y` and an open cover `𝒰` of `Y`, then the property `P` holds for the morphism `f` if and only if `P` holds for the second projection of the pullback (`CategoryTheory.Limits.pullback.snd`) for every index `i` in the index set of the open cover `𝒰`. In other words, a property of a morphism between algebraic schemes is local at the target if it holds for a morphism if and only if it holds for the second projection of the pullback over all elements of any open cover of the target scheme.
More concisely: For any morphism property in the category of algebraic schemes, if it is local at the target, then the property holds for the morphism if and only if it holds for the second projection of the pullback over every index in the open cover of the target scheme.
|
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.toBasicOpen
theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.toBasicOpen :
∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
P.IsLocal →
∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y)
(r : ↑(Y.presheaf.obj (Opposite.op ⊤))), P f → P (f ∣_ Y.basicOpen r)
This theorem states that if a property `P`, which is a class of morphisms from an arbitrary mathematical scheme into an affine scheme, is local, then it remains stable under restriction to the basic open set of global sections. In other words, if `P` holds for a morphism `f` from `X` to `Y`, where `Y` is an affine scheme, and `r` is a global section of `Y`, then `P` also holds for the morphism from `X` to the basic open subset of `Y` determined by `r`.
More concisely: If `P` is a local property of morphisms from schemes to affine schemes, then `P` is preserved under restriction to the basic open subset of a global section.
|
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.ofBasicOpenCover
theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.ofBasicOpenCover :
∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
P.IsLocal →
∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine Y] (f : X ⟶ Y)
(s : Finset ↑(Y.presheaf.obj (Opposite.op ⊤))),
Ideal.span ↑s = ⊤ → (∀ (r : { x // x ∈ s }), P (f ∣_ Y.basicOpen ↑r)) → P f
This theorem states that if a certain property `P` related to morphisms from an arbitrary scheme into an affine scheme holds locally, then it also holds globally on the basic open sets of a spanning set of the global sections. More specifically, given any scheme `X` and any `Y` that is an affine scheme, and a morphism `f` from `X` to `Y`, if we take a finite set `s` of the global sections of the presheaf of `Y` such that the ideal generated by `s` equals the whole ring, if `P` holds for `f` restricted to the basic open sets in `s`, then `P` also holds for `f`.
More concisely: If a property `P` holds locally at the basic open sets of a finite set `s` of global sections generating the entire ring of an affine scheme `Y`, then `P` holds globally for morphisms from an arbitrary scheme `X` into `Y`.
|
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocallyIsLocal
theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocallyIsLocal :
∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
P.IsLocal → AlgebraicGeometry.PropertyIsLocalAtTarget (AlgebraicGeometry.targetAffineLocally P)
The theorem `AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.targetAffineLocallyIsLocal` states that for any `AffineTargetMorphismProperty`, denoted `P`, if `P` is local (as per the definition of being local in the context of `AffineTargetMorphismProperty`), then the property of being affine locally at the target (denoted `AlgebraicGeometry.targetAffineLocally P`) is also local. In other words, if a property `P` holds for all morphisms from any scheme into an affine scheme, and this property is local, then `P` also holds locally at every affine open subset of the target scheme.
More concisely: If `P` is a local property of `AffineTargetMorphisms` in Lean 4, then the property `AlgebraicGeometry.targetAffineLocally P` of being affine locally at the target of `P` is also local.
|
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.RespectsIso
theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.RespectsIso :
∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty}, P.IsLocal → P.toProperty.RespectsIso
The theorem `AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.RespectsIso` states that for any property `P` of a category of morphisms from an arbitrary scheme into an affine scheme, if `P` is a local property (that is, it is satisfied by a morphism if and only if it is satisfied on all localizations), then `P` respects isomorphisms. In other words, if a morphism has property `P` and is isomorphic to another morphism, then the latter morphism also has property `P`.
More concisely: If `P` is a local property of morphisms from schemes to affine schemes, then `P` is preserved under isomorphisms.
|
AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_iff
theorem AlgebraicGeometry.AffineTargetMorphismProperty.IsLocal.affine_openCover_iff :
∀ {P : AlgebraicGeometry.AffineTargetMorphismProperty},
P.IsLocal →
∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
[h𝒰 : ∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)],
AlgebraicGeometry.targetAffineLocally P f ↔ ∀ (i : 𝒰.J), P CategoryTheory.Limits.pullback.snd
This theorem provides a characterization of a property of morphisms between algebraic geometry schemes, when the target is locally affine. Specifically, for any property `P` of morphisms into an affine scheme that is local in the sense of the `AffineTargetMorphismProperty.IsLocal` definition, a morphism `f` from a scheme `X` to a scheme `Y` satisfies the `targetAffineLocally` relation with `P` if and only if `P` holds for the second projection of the pullback of `f` and the inclusion of each open subset of an open cover `𝒰` of `Y`, whenever each object of `𝒰` is an affine scheme.
In simpler terms, this theorem allows us to check a local property on all affine parts of the target of a morphism, rather than on the whole scheme.
More concisely: Given a property `P` of morphisms into affine schemes that is local, a morphism `f` from a scheme `X` to a locally affine scheme `Y` satisfies `P` if and only if `P` holds for the second projection of the pullback and the inclusion of each open subset of any open cover of `Y` that consists of affine schemes.
|