Theorems · Definition · algebraic geometry

AlgebraicGeometry.Smooth.casesOn

{X Y : AlgebraicGeometry.Scheme} →
  {f : X ⟶ Y} →
    {motive : AlgebraicGeometry.Smooth f → Sort u_1} →
      (t : AlgebraicGeometry.Smooth f) →
        ((smooth_appLE :
              ∀ {U : Y.Opens},
                AlgebraicGeometry.IsAffineOpen U →
                  ∀ {V : X.Opens},
                    AlgebraicGeometry.IsAffineOpen V →
                      ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
                        (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Smooth) →
            motive ⋯) →
          motive t

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Smooth

Cited by

1 results in Mathlib

Foundations

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