def KLocallyRingedSpace.Hom.toFun {K : Type}
  [RCLike K] {X Y : KLocallyRingedSpace K}
  (f : X ⟶ Y) :
  ↑↑X.toPresheafedSpace →
    ↑↑Y.toPresheafedSpace :=
  (CategoryTheory.ConcreteCategory.hom
      (↑f).base)
    x

def KLocallyRingedSpace.instCategory
  {K : Type} [RCLike K] :
  CategoryTheory.Category.{u, u + 1}
    (KLocallyRingedSpace K)

def KLocallyRingedSpace.restrictOpen
  {K : Type} [RCLike K]
  (X : KLocallyRingedSpace K)
  (U : Opens ↑↑X.toPresheafedSpace) :
  KLocallyRingedSpace K :=
  let __LocallyRingedSpace :=
    X.restrict ⋯;
  {
    toLocallyRingedSpace :=
      __LocallyRingedSpace,
    algebraMap :=
      (CommRingCat.Hom.hom
            (AlgebraicGeometry.LocallyRingedSpace.Γ.map
              (X.ofRestrict ⋯).op)).comp
        X.algebraMap }

def KLocallyRingedSpace.ofRestrict {K : Type}
  [RCLike K] (X : KLocallyRingedSpace K)
  (U : Opens ↑↑X.toPresheafedSpace) :
  X.restrictOpen U ⟶ X :=
  ⟨X.ofRestrict ⋯, ⋯⟩

def KLocallyRingedSpace.Hom.ofFac {K : Type}
  [RCLike K]
  {A B X : KLocallyRingedSpace K}
  (a : A ⟶ X) (b : B ⟶ X)
  (l :
    A.toLocallyRingedSpace ⟶
      B.toLocallyRingedSpace)
  (hl : l ≫ ↑b = ↑a) : A ⟶ B :=
  ⟨l, ⋯⟩

def KLocallyRingedSpace.instCoeSortType
  {K : Type} [RCLike K] :
  CoeSort (KLocallyRingedSpace K) (Type u)

def KLocallyRingedSpace.ofManifold (K : Type)
  [RCLike K] (E : Type u_1)
  [NormedAddCommGroup E] [NormedSpace K E]
  (M : Type u) [TopologicalSpace M]
  [ChartedSpace E M] :
  KLocallyRingedSpace K :=
  { carrier := ↧M,
    presheaf :=
      (structureSheaf K E M).presheaf,
    IsSheaf := ⋯, isLocalRing := ⋯,
    algebraMap := constHom K E M }

def KLocallyRingedSpace.ofManifoldBase
  {K : Type} [RCLike K] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace K E]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace K E'] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {N : Type u} [TopologicalSpace N]
  [ChartedSpace E' N] (f : M → N)
  (hf : ContMDiff 𝓘(K, E) 𝓘(K, E') ⊤ f) :
  ↧M ⟶ ↧N :=
  TopCat.ofHom
    { toFun := f, continuous_toFun := ⋯ }

def KLocallyRingedSpace.ofManifoldSheafHom
  {K : Type} [RCLike K] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace K E]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace K E'] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {N : Type u} [TopologicalSpace N]
  [ChartedSpace E' N] (f : M → N)
  (hf : ContMDiff 𝓘(K, E) 𝓘(K, E') ⊤ f) :
  (structureSheaf K E' N).presheaf ⟶
    (TopCat.Presheaf.pushforward
          CommRingCat
          (KLocallyRingedSpace.ofManifoldBase
            f hf)).obj
      (structureSheaf K E M).presheaf :=
  {
    app := fun U =>
      CommRingCat.ofHom
        {
          toFun := fun g =>
            ⟨↑g ∘
                (Opposite.unop
                        U).1.restrictPreimage
                  f,
              ⋯⟩,
          map_one' := ⋯, map_mul' := ⋯,
          map_zero' := ⋯, map_add' := ⋯ },
    naturality := ⋯ }

def KLocallyRingedSpace.ofManifoldHomAux
  {K : Type} [RCLike K] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace K E]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace K E'] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {N : Type u} [TopologicalSpace N]
  [ChartedSpace E' N] (f : M → N)
  (hf : ContMDiff 𝓘(K, E) 𝓘(K, E') ⊤ f) :
  (KLocallyRingedSpace.ofManifold K E
        M).toPresheafedSpace ⟶
    (KLocallyRingedSpace.ofManifold K E'
        N).toPresheafedSpace :=
  {
    base :=
      KLocallyRingedSpace.ofManifoldBase f
        hf,
    c :=
      KLocallyRingedSpace.ofManifoldSheafHom
        f hf }

def KLocallyRingedSpace.ofManifoldHom
  {K : Type} [RCLike K] {E : Type u_1}
  [NormedAddCommGroup E] [NormedSpace K E]
  {E' : Type u_2} [NormedAddCommGroup E']
  [NormedSpace K E'] {M : Type u}
  [TopologicalSpace M] [ChartedSpace E M]
  {N : Type u} [TopologicalSpace N]
  [ChartedSpace E' N] (f : M → N)
  (hf : ContMDiff 𝓘(K, E) 𝓘(K, E') ⊤ f) :
  KLocallyRingedSpace.ofManifold K E M ⟶
    KLocallyRingedSpace.ofManifold K E' N :=
  ⟨let __spread.0 :=
      KLocallyRingedSpace.ofManifoldHomAux
        f hf;
    { toHom := __spread.0, prop := ⋯ },
    ⋯⟩

def toSpace {K : Type} [RCLike K]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace K E] {n : ℕ}
  (ψ : E ≃L[K] Fin n → K)
  (M : AnalyticManifold K E) :
  AnalyticSpace K :=
  let __KLocallyRingedSpace :=
    KLocallyRingedSpace.ofManifold K E
      M.carrier;
  {
    toKLocallyRingedSpace :=
      __KLocallyRingedSpace,
    locallyModel := ⋯, t2 := ⋯,
    sigmaCompact := ⋯ }

def toSpaceHom {K : Type} [RCLike K]
  {E : Type u_1} [NormedAddCommGroup E]
  [NormedSpace K E] {n : ℕ}
  (ψ : E ≃L[K] Fin n → K)
  {M N : AnalyticManifold K E}
  (f : AnalyticMap M N) :
  toSpace ψ M ⟶ toSpace ψ N :=
  KLocallyRingedSpace.ofManifoldHom ⇑f ⋯

def affine (K : Type) [RCLike K] (n : ℕ) :
  KLocallyRingedSpace K :=
  KLocallyRingedSpace.ofManifold K
    (Kn K n) (Kn K n)

def analyticSpaceOfOpen (K : Type) [RCLike K]
  (n : ℕ) (G : Opens (Kn K n)) :
  KLocallyRingedSpace K :=
  (affine K n).restrictOpen G

def toGlobal (K : Type) [RCLike K] (n : ℕ)
  (G : Opens (Kn K n)) :
  AnalyticFun K n G →+*
    ↑((analyticSpaceOfOpen K n
              G).presheaf.obj
        (Opposite.op ⊤)) :=
  CommRingCat.Hom.hom
    ((affine K n).presheaf.map
      (CategoryTheory.homOfLE ⋯).op)

def IdealSheaf.ofGlobal {X : TopCat}
  (𝒪 : TopCat.Sheaf CommRingCat X) {k : ℕ}
  (f :
    Fin k →
      ↑(𝒪.presheaf.obj (Opposite.op ⊤))) :
  Manifold.IdealSheaf 𝒪 :=
  IdealSheaf.ofStalks 𝒪
    (fun x =>
      Ideal.span
        (range fun i =>
          (CategoryTheory.ConcreteCategory.hom
              (𝒪.presheaf.germ ⊤ x
                trivial))
            (f i)))
    ⋯

def modelIdeal (K : Type) [RCLike K] (n : ℕ)
  (G : Opens (Kn K n)) {k : ℕ}
  (f : Fin k → AnalyticFun K n G) :
  Manifold.IdealSheaf
    (analyticSpaceOfOpen K n G).𝒪 :=
  IdealSheaf.ofGlobal
    (analyticSpaceOfOpen K n G).𝒪 fun i =>
    (toGlobal K n G) (f i)

def localModel (K : Type) [RCLike K] (n : ℕ)
  (G : Opens (Kn K n)) {k : ℕ}
  (f : Fin k → AnalyticFun K n G) :
  KLocallyRingedSpace K :=
  (analyticSpaceOfOpen K n G).quotient
    (modelIdeal K n G f)

def QuotientSpace.support
  (X :
    AlgebraicGeometry.LocallyRingedSpace)
  (J : Manifold.IdealSheaf X.𝒪) : TopCat :=
  ↧↑J.support

def QuotientSpace.localPred
  (X :
    AlgebraicGeometry.LocallyRingedSpace)
  (J : Manifold.IdealSheaf X.𝒪) :
  TopCat.LocalPredicate
    (QuotientSpace.fiber X J) :=
  (QuotientSpace.prelocalPred X
      J).sheafify

def QuotientSpace.sheafTypes
  (X :
    AlgebraicGeometry.LocallyRingedSpace)
  (J : Manifold.IdealSheaf X.𝒪) :
  TopCat.Sheaf (Type u)
    (QuotientSpace.support X J) :=
  TopCat.subsheafToTypes
    (QuotientSpace.localPred X J)