-- Mathlib/AlgebraicGeometry/Morphisms/OpenImmersion.lean
/-- `Spec (R ⧸ I) ⟶ Spec R` is an open immersion iff `I` is generated by an idempotent. -/
lemma isOpenImmersion_SpecMap_iff_of_surjective {R S : CommRingCat}
    (f : R ⟶ S) (hf : Function.Surjective f.hom) :
    IsOpenImmersion (Spec.map f) ↔
    ∃ e, IsIdempotentElem e ∧ RingHom.ker f.hom = Ideal.span {e}

Proof state:
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(ConcreteCategory.hom (Spec.map φ).base) = Set.range ⇑(ConcreteCategory.hom (Spec.map f).base)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
⊢ f = φ ≫ i.inv

Tactic:
apply Spec.map_injective

Result:
case a
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(ConcreteCategory.hom (Spec.map φ).base) = Set.range ⇑(ConcreteCategory.hom (Spec.map f).base)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
⊢ Spec.map f = Spec.map (φ ≫ i.inv)

Proof state:
case mp.intro.intro
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
have : IsOpenImmersion (Spec.map φ) :=
  have : IsLocalization.Away (1 - e) (↑R ⧸ Ideal.span {e}) :=
    IsLocalization.away_of_isIdempotentElem he.one_sub (by simp) Ideal.Quotient.mk_surjective
  IsOpenImmersion.of_isLocalization (1 - e)

Result:
case mp.intro.intro
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Proof state:
case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ IsOpenImmersion (Spec.map f) → ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
intro H

Result:
case mp
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H : IsOpenImmersion (Spec.map f)
⊢ ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Proof state:
case mp.intro.intro
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(ConcreteCategory.hom (Spec.map φ).base) = Set.range ⇑(ConcreteCategory.hom (Spec.map f).base)
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
let i : S ≅ .of _ := (Scheme.Spec.preimageIso
  (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop

Result:
case mp.intro.intro
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range ⇑(PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := CommRingCat.ofHom (Ideal.Quotient.mk (Ideal.span {e}))
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(ConcreteCategory.hom (Spec.map φ).base) = Set.range ⇑(ConcreteCategory.hom (Spec.map f).base)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) :=
  (Scheme.Spec.preimageIso (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
⊢ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Proof state:
case mpr.intro.intro
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
e : ↑R
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}
⊢ IsOpenImmersion (Spec.map f)

Tactic:
letI := f.hom.toAlgebra

Result:
case mpr.intro.intro
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
e : ↑R
he : IsIdempotentElem e
he' : RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}
this : Algebra ↑R ↑S := (CommRingCat.Hom.hom f).toAlgebra
⊢ IsOpenImmersion (Spec.map f)