∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  (∀ {U : TopologicalSpace.Opens ↥Y},
      AlgebraicGeometry.IsAffineOpen U →
        ∀ {V : TopologicalSpace.Opens ↥X},
          AlgebraicGeometry.IsAffineOpen V →
            ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Etale) ↔
    (∀ {U : TopologicalSpace.Opens ↥Y},
        AlgebraicGeometry.IsAffineOpen U →
          ∀ {V : TopologicalSpace.Opens ↥X},
            AlgebraicGeometry.IsAffineOpen V →
              ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
                (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).Flat) ∧
      (∀ {U : TopologicalSpace.Opens ↥Y},
          AlgebraicGeometry.IsAffineOpen U →
            ∀ {V : TopologicalSpace.Opens ↥X},
              AlgebraicGeometry.IsAffineOpen V →
                ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
                  (CategoryTheory.ConcreteCategory.hom
                      (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FormallyUnramified) ∧
        ∀ {U : TopologicalSpace.Opens ↥Y},
          AlgebraicGeometry.IsAffineOpen U →
            ∀ {V : TopologicalSpace.Opens ↥X},
              AlgebraicGeometry.IsAffineOpen V →
                ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
                  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FinitePresentation