Theorems · Theorem · algebraic geometry

AlgebraicGeometry.topologically_respectsIso

∀ (P : {α β : Type u} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop),
  (∀ {α β : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β), P ⇑f) →
    (∀ {α β γ : Type u} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ]
        (f : α → β) (g : β → γ), P f → P g → P (g ∘ f)) →
      (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => P).RespectsIso

If a property of maps of topological spaces is satisfied by homeomorphisms and is stable under composition, the induced property on schemes respects isomorphisms.

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Constructors

Cited by

0 results in Mathlib

Foundations

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