Theorems · Definition · algebraic geometry

AlgebraicGeometry.SmoothOfRelativeDimension.recOn

{n : ℕ} →
  {X Y : AlgebraicGeometry.Scheme} →
    {f : X ⟶ Y} →
      {motive : AlgebraicGeometry.SmoothOfRelativeDimension n f → Sort u_1} →
        (t : AlgebraicGeometry.SmoothOfRelativeDimension n f) →
          ((exists_isStandardSmoothOfRelativeDimension :
                ∀ (x : ↥X),
                  ∃ U,
                    ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
                      ∃ V,
                        ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (_ : x ∈ V) (e :
                          V ≤ (TopologicalSpace.Opens.map f.base).obj U),
                          RingHom.IsStandardSmoothOfRelativeDimension n
                            (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e))) →
              motive ⋯) →
            motive t

Defined in

Mathlib.AlgebraicGeometry.Morphisms.Smooth

Cited by

0 results in Mathlib

Foundations

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