Documentation

Mathlib.AlgebraicGeometry.Morphisms.LocalClosure

Local closure of morphism properties #

We define the source local closure of a property P wrt. a morphism property W and show it inherits stability properties from P.

source
def AlgebraicGeometry.sourceLocalClosure (W P : CategoryTheory.MorphismProperty Scheme) :
CategoryTheory.MorphismProperty Scheme

The source (Zariski-)local closure of P is satisfied if there exists an open cover of the source on which P is satisfied.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.sourceLocalClosure.cover {W P : CategoryTheory.MorphismProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} (hf : sourceLocalClosure W P f) :
    Scheme.Cover W X

    A choice of open cover on which P is satisfied if f satisfies the source local closure of P.

    Equations
    Instances For
      source
      theorem AlgebraicGeometry.sourceLocalClosure.property_coverMap_comp {W P : CategoryTheory.MorphismProperty Scheme} {X Y : Scheme} {f : X ⟶ Y} (hf : sourceLocalClosure W P f) (i : hf.cover.J) :
      P (CategoryTheory.CategoryStruct.comp (hf.cover.map i) f)
      source
      theorem AlgebraicGeometry.sourceLocalClosure.le {W P : CategoryTheory.MorphismProperty Scheme} [W.ContainsIdentities] [W.RespectsIso] :
      P ≤ sourceLocalClosure W P
      source
      theorem AlgebraicGeometry.sourceLocalClosure.iff_forall_exists {P : CategoryTheory.MorphismProperty Scheme} {X Y : Scheme} [P.RespectsIso] {f : X ⟶ Y} :
      sourceLocalClosure IsOpenImmersion P f ↔ ∀ (x : ↥X), ∃ (U : X.Opens), x ∈ U ∧ P (CategoryTheory.CategoryStruct.comp U.ι f)
      source
      instance AlgebraicGeometry.sourceLocalClosure.instRespectsLeftSchemeOfIsStableUnderBaseChange {W P Q : CategoryTheory.MorphismProperty Scheme} [W.IsStableUnderBaseChange] [Scheme.IsJointlySurjectivePreserving W] [P.RespectsLeft Q] [Q.IsStableUnderBaseChange] :
      (sourceLocalClosure W P).RespectsLeft Q
      source
      instance AlgebraicGeometry.sourceLocalClosure.instRespectsRightScheme {W P Q : CategoryTheory.MorphismProperty Scheme} [P.RespectsRight Q] :
      (sourceLocalClosure W P).RespectsRight Q
      source
      instance AlgebraicGeometry.sourceLocalClosure.instRespectsIsoScheme {W P : CategoryTheory.MorphismProperty Scheme} [W.IsStableUnderBaseChange] [Scheme.IsJointlySurjectivePreserving W] [P.RespectsIso] :
      (sourceLocalClosure W P).RespectsIso
      source
      instance AlgebraicGeometry.sourceLocalClosure.instIsLocalAtSourceIsOpenImmersionOfRespectsIsoOfRespectsLeftScheme {P : CategoryTheory.MorphismProperty Scheme} [P.RespectsIso] [P.RespectsLeft IsOpenImmersion] :
      IsLocalAtSource (sourceLocalClosure IsOpenImmersion P)
      source
      instance AlgebraicGeometry.sourceLocalClosure.instIsStableUnderBaseChangeScheme {W P : CategoryTheory.MorphismProperty Scheme} [W.IsStableUnderBaseChange] [Scheme.IsJointlySurjectivePreserving W] [P.IsStableUnderBaseChange] :
      (sourceLocalClosure W P).IsStableUnderBaseChange
      source
      instance AlgebraicGeometry.sourceLocalClosure.instContainsIdentitiesScheme {W P : CategoryTheory.MorphismProperty Scheme} [W.IsStableUnderBaseChange] [W.ContainsIdentities] [P.ContainsIdentities] :
      (sourceLocalClosure W P).ContainsIdentities
      source
      instance AlgebraicGeometry.sourceLocalClosure.instIsStableUnderCompositionSchemeOfIsStableUnderBaseChange {W P : CategoryTheory.MorphismProperty Scheme} [W.IsStableUnderBaseChange] [Scheme.IsJointlySurjectivePreserving W] [W.IsStableUnderComposition] [P.IsStableUnderBaseChange] [P.IsStableUnderComposition] :
      (sourceLocalClosure W P).IsStableUnderComposition
      source
      instance AlgebraicGeometry.sourceLocalClosure.instIsMultiplicativeSchemeOfIsStableUnderBaseChange {W P : CategoryTheory.MorphismProperty Scheme} [W.IsStableUnderBaseChange] [Scheme.IsJointlySurjectivePreserving W] [W.IsMultiplicative] [P.IsStableUnderBaseChange] [P.IsMultiplicative] :
      (sourceLocalClosure W P).IsMultiplicative