preimage_comp — Mathlib

English

For G ⊆ F and morphisms f: F'' → F' and g: F' → F, the preimage under f ≫ g equals the preimage under g followed by the preimage under f.

Русский

Для подпреша G ⊆ F и морфизмов f: F'' → F' и g: F' → F, предобраз f ≫ g равен предобразу g затем предобразу f.

LaTeX

$$$ G.\\mathrm{preimage}(f \\ggg g) = (G.\\mathrm{preimage} g).\\mathrm{preimage} f $$$

Lean4

theorem preimage_comp (G : Subpresheaf F) (f : F'' ⟶ F') (g : F' ⟶ F) :
    G.preimage (f ≫ g) = (G.preimage g).preimage f := by aesop

Похожие утверждения