pre_semi_sheaves.lean

import algebra.ring 

structure pre_semi_sheaf_of_rings (α : Type) := 
(F : Π (U : set α), Type)
[Fring : ∀ (U : set α), comm_ring (F U)]

attribute [instance] pre_semi_sheaf_of_rings.Fring

structure morphism_of_pre_semi_sheaves_of_rings {α : Type}
  (FPT : pre_semi_sheaf_of_rings α) (GPT : pre_semi_sheaf_of_rings α) :=
(morphism : ∀ U : set α, (FPT.F U) → GPT.F U)
(ring_homs : ∀ U : set α, @is_ring_hom _ _ _ _ (morphism U))

attribute [instance]  morphism_of_pre_semi_sheaves_of_rings.ring_homs

def is_identity_morphism_of_pre_semi_sheaves_of_rings {α : Type}
  {FPT : pre_semi_sheaf_of_rings α} (phi: morphism_of_pre_semi_sheaves_of_rings FPT FPT) :=
  ∀ (U : set α), phi.morphism U = id

def composition_of_morphisms_of_pre_semi_sheaves_of_rings {α : Type}
  {FPT GPT HPT : pre_semi_sheaf_of_rings α} (fg : morphism_of_pre_semi_sheaves_of_rings FPT GPT)
  (gh : morphism_of_pre_semi_sheaves_of_rings GPT HPT) :
morphism_of_pre_semi_sheaves_of_rings FPT HPT :=
{ morphism := λ U, gh.morphism U ∘ fg.morphism U,
  ring_homs := λ U, is_ring_hom.comp _ _ -- composition of two ring homs is a ring hom done by type class inference
}


def are_isomorphic_pre_semi_sheaves_of_rings {α : Type}
  (FPR : pre_semi_sheaf_of_rings α) (GPR : pre_semi_sheaf_of_rings α) : Prop := 
∃ (fg : morphism_of_pre_semi_sheaves_of_rings FPR GPR) (gf : morphism_of_pre_semi_sheaves_of_rings GPR FPR),
  is_identity_morphism_of_pre_semi_sheaves_of_rings (composition_of_morphisms_of_pre_semi_sheaves_of_rings fg gf)
  ∧ is_identity_morphism_of_pre_semi_sheaves_of_rings (composition_of_morphisms_of_pre_semi_sheaves_of_rings gf fg)

definition pre_semi_sheaf_of_rings_pullback
  {α : Type}
  {β : Type}
  (PR : pre_semi_sheaf_of_rings β)
  (f : α → β)
  : pre_semi_sheaf_of_rings α :=
{ F := λ V,PR.F (f '' V)
}

theorem pre_semi_sheaves_iso (X : Type) (F : pre_semi_sheaf_of_rings X) : 
are_isomorphic_pre_semi_sheaves_of_rings
    (pre_semi_sheaf_of_rings_pullback F id) F
:= sorry