SigmaRepresenter.lean

def coverRestrictionObject (T : X.Etale) (i : 𝒰.I₀) : X.Etale

def coverRestrictionMap (T : X.Etale) (i : 𝒰.I₀) :
    coverRestrictionObject 𝒰 T i ⟶ T

lemma coverRestrictionSieve_mem (T : X.Etale) :
    Sieve.ofArrows (coverRestrictionObject 𝒰 T) (coverRestrictionMap 𝒰 T) ∈
      X.smallEtaleTopology T

lemma isIso_of_bijective_on_etaleCover
    {F G : Sheaf X.smallEtaleTopology (Type u)} (η : F ⟶ G)
    (h : ∀ (i : 𝒰.I₀) (T : (𝒰.X i).Etale),
      Function.Bijective (η.hom.app (op ((etalePostcompose (𝒰.f i)).obj T)))) :
    IsIso η

def etaleSigma : X.Etale

def etaleSigmaInj (i : ι) : U i ⟶ etaleSigma U

def isInitialEtaleOfEmpty (T : X.Etale) [IsEmpty T.left] : IsInitial T

lemma emptyEtaleCover (T : X.Etale) (hT : IsInitial T) :
    ⊥ ∈ X.smallEtaleTopology T

def etaleSigmaYonedaIsColimit :
    IsColimit (Cofan.mk (X.smallEtaleTopology.yoneda.obj (etaleSigma U))
      (fun i => X.smallEtaleTopology.yoneda.map (etaleSigmaInj U i))) := by
  have (i : ι) : Mono ((Cofan.mk (etaleSigma U) (etaleSigmaInj U)).inj i) := by
    constructor
    intro T a b hab
    apply MorphismProperty.Over.Hom.ext
    exact (cancel_mono (Sigma.ι (fun j => (U j).left) i)).mp
      (congrArg (fun f => f.left) hab)
  apply X.smallEtaleTopology.isColimitCofanMkYoneda U
    (c := Cofan.mk (etaleSigma U) (etaleSigmaInj U))
  · rw [Scheme.ofArrows_mem_smallEtaleTopology_iff]
    exact Scheme.Cover.iUnion_range (sigmaOpenCover (fun i => (U i).left))
  · exact emptyEtaleCover
  · intro i j hij T a b hab
    have : IsEmpty T.left := isEmpty_of_commSq_sigmaι_of_ne
      ⟨congrArg (fun f => f.left) hab⟩ hij
    exact ⟨isInitialEtaleOfEmpty T⟩

def etaleSigmaSheafHom (G : Sheaf X.smallEtaleTopology (Type u))
    (s : ∀ i : ι, G.obj.obj (op (U i))) :
    X.smallEtaleTopology.yoneda.obj (etaleSigma U) ⟶ G

lemma etaleSigmaSheafHom_comp (G : Sheaf X.smallEtaleTopology (Type u))
    (s : ∀ i : ι, G.obj.obj (op (U i))) (i : ι) :
    X.smallEtaleTopology.yoneda.map (etaleSigmaInj U i) ≫ etaleSigmaSheafHom U G s =
      X.smallEtaleTopology.yonedaEquiv.symm (s i)

lemma etaleSigmaSheafHom_apply_component (G : Sheaf X.smallEtaleTopology (Type u))
    (s : ∀ i : ι, G.obj.obj (op (U i))) (i : ι) {T : X.Etale} (f : T ⟶ U i) :
    (etaleSigmaSheafHom U G s).hom.app (op T) (f ≫ etaleSigmaInj U i) =
      G.obj.map f.op (s i)

def etaleSigmaSection (G : Sheaf X.smallEtaleTopology (Type u))
    (s : ∀ i : ι, G.obj.obj (op (U i))) : G.obj.obj (op (etaleSigma U))

lemma etaleSigmaSection_restrict (G : Sheaf X.smallEtaleTopology (Type u))
    (s : ∀ i : ι, G.obj.obj (op (U i))) (i : ι) :
    G.obj.map (etaleSigmaInj U i).op (etaleSigmaSection U G s) = s i

lemma etalePostcompose_hom_bijective_of_isPullback
    {A B : Scheme.{u}} (f : A ⟶ B) [Etale f] (W : A.Etale) (V : B.Etale)
    (k : (etalePostcompose f).obj W ⟶ V)
    (h : IsPullback W.hom k.left f V.hom) (T : A.Etale) :
    Function.Bijective (fun g : T ⟶ W => (etalePostcompose f).map g ≫ k) := by
  constructor
  · intro g g' hgg'
    apply MorphismProperty.Over.Hom.ext
    apply h.hom_ext
    · exact g.w.trans g'.w.symm
    · exact congrArg (fun e => e.left) hgg'
  · intro g
    let l : T ⟶ W := MorphismProperty.Over.homMk
      (h.lift T.hom g.left g.w.symm) (h.lift_fst T.hom g.left g.w.symm)
    refine ⟨l, ?_⟩
    apply MorphismProperty.Over.Hom.ext
    exact h.lift_snd T.hom g.left g.w.symm

def sigmaRepresentableBy {ι : Type v} [Small.{u} ι] (U : ι → Scheme.{u})
    (G : Sheaf (∐ U).smallEtaleTopology (Type u)) (W : ∀ i : ι, (U i).Etale)
    (h : ∀ i : ι, ((etalePostcompose (Sigma.ι U i)).op ⋙ G.obj).RepresentableBy (W i)) :
    G.obj.RepresentableBy
      (etaleSigma (fun i => (etalePostcompose (Sigma.ι U i)).obj (W i))) := by
  let Z : ι → (∐ U).Etale := fun i => (etalePostcompose (Sigma.ι U i)).obj (W i)
  let s : ∀ i : ι, G.obj.obj (op (Z i)) := fun i => (h i).homEquiv (𝟙 (W i))
  let η := etaleSigmaSheafHom Z G s
  have hη : IsIso η := by
    apply isIso_of_bijective_on_etaleCover
      ((sigmaOpenCover U).changeProp (Q := show MorphismProperty Scheme.{u} from @Etale)
        (fun i => inferInstance)) η
    intro i T
    have hCart : IsPullback (W i).hom (etaleSigmaInj Z i).left
        (Sigma.ι U i) (etaleSigma Z).hom :=
      isPullback_sigmaι_sigmaMap (fun j => (W j).hom) i
    have hHom := etalePostcompose_hom_bijective_of_isPullback
      (Sigma.ι U i) (W i) (etaleSigma Z) (etaleSigmaInj Z i) hCart T
    apply (Function.Bijective.of_comp_iff _ hHom).mp
    have heq : (fun g : T ⟶ W i =>
        η.hom.app (op ((etalePostcompose (Sigma.ι U i)).obj T))
          ((etalePostcompose (Sigma.ι U i)).map g ≫ etaleSigmaInj Z i)) =
        (h i).homEquiv := by
      funext g
      exact (etaleSigmaSheafHom_apply_component Z G s i
        ((etalePostcompose (Sigma.ι U i)).map g)).trans
          ((h i).homEquiv_eq g).symm
    change Function.Bijective (fun g : T ⟶ W i =>
      η.hom.app (op ((etalePostcompose (Sigma.ι U i)).obj T))
        ((etalePostcompose (Sigma.ι U i)).map g ≫ etaleSigmaInj Z i))
    rw [heq]
    exact (h i).homEquiv.bijective
  exact Functor.representableByEquiv.symm
    ((sheafToPresheaf (∐ U).smallEtaleTopology (Type u)).mapIso (asIso η))

def etaleSigmaRestrictionRepresentableBy {ι : Type v} [Small.{u} ι]
    (U : ι → X.Etale) (G : Sheaf X.smallEtaleTopology (Type u))
    (W : ∀ i : ι, (U i).left.Etale)
    (h : ∀ i : ι, ((etalePostcompose (U i).hom).op ⋙ G.obj).RepresentableBy (W i)) :
    ((etalePostcompose (hf := (etaleSigma U).prop) (etaleSigma U).hom).op ⋙ G.obj).RepresentableBy
      (etaleSigma (fun i =>
        (etalePostcompose (Sigma.ι (fun j => (U j).left) i)).obj (W i))) := by
  apply sigmaRepresentableBy (fun i => (U i).left)
    ((etaleRestriction (hf := (etaleSigma U).prop) (etaleSigma U).hom (Type u)).obj G) W
  intro i
  let e : etalePostcompose (U i).hom ≅
      etalePostcompose (Sigma.ι (fun j => (U j).left) i) ⋙
        etalePostcompose (hf := (etaleSigma U).prop) (etaleSigma U).hom :=
    MorphismProperty.Over.mapComp
      (P := show MorphismProperty Scheme.{u} from @Etale) ⊤
      (inferInstance : Etale (Sigma.ι (fun j => (U j).left) i))
      (etaleSigma U).prop (U i).hom (Sigma.ι_comp_desc (fun j => (U j).hom) i).symm
  exact (h i).ofIso (Functor.isoWhiskerRight (NatIso.op e).symm G.obj)

def finiteEtaleSigma {ι : Type v} [Small.{u} ι] (U : ι → Scheme.{u})
    (W : ∀ i : ι, FiniteEtale (U i)) : FiniteEtale (∐ U)

def finiteEtaleSigmaRestrictionRepresentableBy {ι : Type v} [Small.{u} ι]
    (U : ι → X.Etale) (G : Sheaf X.smallEtaleTopology (Type u))
    (W : ∀ i : ι, FiniteEtale (U i).left)
    (h : ∀ i : ι, ((etalePostcompose (U i).hom).op ⋙ G.obj).RepresentableBy
      ((finiteEtaleToEtale (U i).left).obj (W i))) :
    ((etalePostcompose (hf := (etaleSigma U).prop) (etaleSigma U).hom).op ⋙ G.obj).RepresentableBy
      ((finiteEtaleToEtale (etaleSigma U).left).obj
        (finiteEtaleSigma (fun i => (U i).left) W)) :=
  etaleSigmaRestrictionRepresentableBy U G
    (fun i => (finiteEtaleToEtale (U i).left).obj (W i)) h