-- Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
/-- A surjective closed immersion is an isomorphism when the target is reduced. -/
lemma isIso_of_isClosedImmersion_of_surjective {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsClosedImmersion f] [Surjective f] [IsReduced Y] :
    IsIso f

Proof state:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ RingHom.ker (CommRingCat.Hom.hom φ) ≤ nilradical ↑Γ(Y, ⊤)

Tactic:
refine (PrimeSpectrum.zeroLocus_eq_top_iff _).mp ?_

Result:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom φ)) = ⊤

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
⊢ IsIso f

Tactic:
wlog hY : IsAffine Y

Result:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
⊢ IsIso f

X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
⊢ IsIso f

Proof state:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ MorphismProperty.isomorphisms Scheme (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
apply (config := { allowSynthFailures := true }) this

Result:
case inst
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom Y.affineCover f i)

case inst
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ Surjective (Scheme.Cover.pullbackHom Y.affineCover f i)

case inst
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ IsReduced (Y.affineCover.obj i)

case inr.hY
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ IsAffine (Y.affineCover.obj i)

Proof state:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
let φ := f.appTop

Result:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Proof state:
case inst
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ Surjective (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
exact IsLocalAtTarget.of_isPullback (.of_hasPullback f (Y.affineCover.map i)) ‹_›

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
this : RingHom.ker (CommRingCat.Hom.hom φ) ≤ nilradical ↑Γ(Y, ⊤)
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Tactic:
rwa [nilradical_eq_zero, Submodule.zero_eq_bot, le_bot_iff,
  ← RingHom.injective_iff_ker_eq_bot] at this

Result:
no goals

Proof state:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
this : Surjective (Spec.map (Scheme.Hom.appTop f))
⊢ Function.Surjective (ConcreteCategory.hom (Scheme.Hom.appTop f)).specComap

Tactic:
exact this.1

Result:
no goals

Proof state:
case inst
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ IsClosedImmersion (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
exact MorphismProperty.pullback_snd _ _ inferInstance

Result:
no goals

Proof state:
case inst
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ IsReduced (Y.affineCover.obj i)

Tactic:
exact isReduced_of_isOpenImmersion (Y.affineCover.map i)

Result:
no goals

Proof state:
case inr.hY
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsClosedImmersion f] [inst : Surjective f] [inst : IsReduced Y],
    IsAffine Y → IsIso f
hY : ¬IsAffine Y
i : Y.affineCover.1
⊢ IsAffine (Y.affineCover.obj i)

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
⊢ IsIso f

Tactic:
apply IsClosedImmersion.isIso_of_injective_of_isAffine

Result:
case hf
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))

Proof state:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom φ)) = ⊤

Tactic:
rw [← range_specComap_of_surjective _ _ hf, Set.top_eq_univ, Set.range_eq_univ]

Result:
case hf.intro
X Y : Scheme
f : X ⟶ Y
inst✝² : IsClosedImmersion f
inst✝¹ : Surjective f
inst✝ : IsReduced Y
hY : IsAffine Y
hX : IsAffine X
hf : Function.Surjective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop f))
φ : Γ(Y, ⊤) ⟶ Γ(X, ⊤) := Scheme.Hom.appTop f
⊢ Function.Surjective (ConcreteCategory.hom (Scheme.Hom.appTop f)).specComap