Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.Hom.appLE_appIso_inv

∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] {U : Y.Opens} {V : X.Opens}
  (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appLE f U V e)
      (AlgebraicGeometry.Scheme.Hom.appIso f V).inv =
    Y.presheaf.map (CategoryTheory.homOfLE ⋯).op

Defined in

Mathlib.AlgebraicGeometry.OpenImmersion

Cited by

2 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsOpenImmersion