Restriction.lean

def ConstructibleStratification.mapIso (S : ConstructibleStratification X) (e : X ≅ Y) :
    ConstructibleStratification Y where
  I := S.I
  finite := S.finite
  stratum := S.stratum
  map i := S.map i ≫ e.hom
  isImmersion i := by
    have : IsImmersion (S.map i) := S.isImmersion i
    infer_instance
  constructible_range i := by
    change Topology.IsConstructible (Set.range (e.hom ∘ S.map i))
    rw [Set.range_comp]
    apply (S.constructible_range i).image_of_isOpenEmbedding e.hom.isOpenEmbedding
    rw [Set.range_eq_univ.mpr e.hom.surjective]
    exact IsRetrocompact.univ
  disjoint := by
    intro i j hij
    apply Set.disjoint_left.mpr
    rintro y ⟨x, hx⟩ ⟨z, hz⟩
    have hxz : S.map i x = S.map j z :=
      e.hom.isOpenEmbedding.injective (hx.trans hz.symm)
    exact (S.disjoint hij).notMem_of_mem_left ⟨x, rfl⟩ ⟨z, hxz.symm⟩
  cover y := by
    obtain ⟨i, x, hx⟩ := S.cover (e.inv y)
    refine ⟨i, x, ?_⟩
    change e.hom (S.map i x) = y
    rw [hx]
    exact congrArg (fun f : Y ⟶ Y => f y) e.inv_hom_id

lemma HasFiniteConstructibleStratification.of_pullbackIso
    (e : X ≅ Y) {G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : HasFiniteConstructibleStratification R ((etalePullback e.hom R).obj G)) :
    HasFiniteConstructibleStratification R G

lemma HasFiniteConstructibleStratification.pullbackIso
    (e : X ≅ Y) {G : Sheaf Y.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : HasFiniteConstructibleStratification R G) :
    HasFiniteConstructibleStratification R ((etalePullback e.hom R).obj G)

theorem isEtaleConstructible_iff_hasFiniteConstructibleStratification [IsAffine X]
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    IsEtaleConstructible R G ↔ HasFiniteConstructibleStratification R G

lemma IsEtaleConstructible.restrict
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)}
    (hG : IsEtaleConstructible R G) (U : X.Opens) :
    IsEtaleConstructible R ((etalePullback U.ι R).obj G)