Theorems · Theorem · algebraic geometry

AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux

∀ (X : AlgebraicGeometry.Scheme) (S : ↑X.affineOpens) (U₁ U₂ : X.Opens) {n₁ n₂ : ℕ}
  {y₁ : ↑(X.presheaf.obj (Opposite.op U₁))} {y₂ : ↑(X.presheaf.obj (Opposite.op U₂))}
  {f : ↑(X.presheaf.obj (Opposite.op (U₁ ⊔ U₂)))} {x : ↑(X.presheaf.obj (Opposite.op (X.basicOpen f)))} (h₁ : ↑S ≤ U₁)
  (h₂ : ↑S ≤ U₂),
  TopCat.Presheaf.restrictOpen y₁ (X.basicOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)) ⋯ =
      TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)
            (X.basicOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)) ⋯ ^
          n₁ *
        TopCat.Presheaf.restrictOpen x (X.basicOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯)) ⋯ →
    TopCat.Presheaf.restrictOpen y₂ (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯ =
        TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)
              (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯ ^
            n₂ *
          TopCat.Presheaf.restrictOpen x (X.basicOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯)) ⋯ →
      ∃ n,
        ∀ (m : ℕ),
          n ≤ m →
            TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯ ^ (m + n₂) * y₁) (↑S) h₁ =
              TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯ ^ (m + n₁) * y₂) (↑S) h₂

Defined in

Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Cited by

1 results in Mathlib

Foundations

Depth 156 from the axioms · uses propext, Classical.choice, Quot.sound