AlgebraicGeometry.IsClosedImmersion.existsUnique_comp_eq_of_range_subset_of_isReduced
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace IsClosedImmersion_existsUnique_comp_eq_of_range_subset_of_isReduced
universe u
open CategoryTheory AlgebraicGeometry TopologicalSpaceLean source · statement
theorem _root_.AlgebraicGeometry.IsClosedImmersion.existsUnique_comp_eq_of_range_subset_of_isReduced
{X Y T : Scheme.{u}} (i : Y ⟶ X) [IsClosedImmersion i] (f : T ⟶ X) [IsReduced T]
(H : Set.range f.base ⊆ Set.range i.base) :
∃! g : T ⟶ Y, g ≫ i = f