English
If f is a morphism with X,Y affine then IsAffineHom f.
Русский
Если X,Y аффинны, то f является IsAffineHom.
LaTeX
$$$[IsAffine X] \\land [IsAffine Y] \\Rightarrow IsAffineHom f$$$
Lean4
instance : HasAffineProperty @IsAffineHom fun X _ _ _ ↦ IsAffine X
where
isLocal_affineProperty := by
constructor
· apply AffineTargetMorphismProperty.respectsIso_mk
· rintro X Y Z e _ _ H
have : IsAffine _ := H
exact .of_isIso e.hom
· exact fun _ _ _ ↦ id
· intro X Y _ f r H
have : IsAffine X := H
change IsAffineOpen _
rw [Scheme.preimage_basicOpen]
exact (isAffineOpen_top X).basicOpen _
· intro X Y _ f S hS hS'
apply_fun Ideal.map (f.appTop).hom at hS
rw [Ideal.map_span, Ideal.map_top] at hS
apply isAffine_of_isAffineOpen_basicOpen _ hS
have : ∀ i : S, IsAffineOpen (f ⁻¹ᵁ Y.basicOpen i.1) := hS'
simpa [Scheme.preimage_basicOpen] using this
eq_targetAffineLocally' := by
ext X Y f
simp only [targetAffineLocally, Scheme.affineOpens, Set.coe_setOf, Set.mem_setOf_eq, Subtype.forall,
isAffineHom_iff]
rfl
