t — Mathlib · SciLib

Lean4
/-- (Implementation detail)
The transition map `V i j ⟶ V j i` in the glue data associated to a locally directed diagram. -/
def t (i j : J) : (V F i j).toScheme ⟶ (V F j i).toScheme :=
  IsOpenImmersion.lift (V F j i).ι (tAux F i j)
    (by
      rintro _ ⟨x, rfl⟩
      obtain ⟨l, x, rfl⟩ := (Scheme.Opens.iSupOpenCover _).exists_eq x
      simp only [V, tAux, ← Scheme.comp_base_apply, Cover.ι_glueMorphisms]
      simp only [Opens.range_ι, iSup_mk, carrier_eq_coe, Hom.coe_opensRange, coe_mk, comp_coeBase, TopCat.hom_comp,
        ContinuousMap.comp_apply]
      exact Set.mem_iUnion.mpr ⟨⟨l.1, l.2.2, l.2.1⟩, ⟨_, rfl⟩⟩)
Похожие утверждения