mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (R[X] ⧸ Ideal.span {g})

Tactic:
·

Goal state after:
case inst
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ Module.Free R (R[X] ⧸ Ideal.span {g})
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.hS
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := ⋯
⊢ ⨆ i, ↑(fS i) = ⊤

pp: case mpr.hS'
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := ⋯
⊢ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(X, ↑(fS i))

Tactic:
·

Goal state after:
case mpr.hS
X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
fS : 𝒰.I₀ → ↑X.affineOpens := ⋯
⊢ ⨆ i, ↑(fS i) = ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0

pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0 ↔ ∃ i, coeff i f ∉ x.asIdeal

Tactic:
·

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.I₀), IsLocallyNoetherian (𝒰.X i)) → IsLocallyNoetherian X

Tactic:
·

Goal state after:
X : Scheme
𝒰 : X.OpenCover
⊢ (∀ (i : 𝒰.I₀), IsLocallyNoetherian (𝒰.X i)) → IsLocallyNoetherian X
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst✝ : IsNoetherianRing ↑Γ(X, U)
⊢ NoetherianSpace ↥↑U

Tactic:
have : IsNoetherianRing Γ(U, ⊤) := isNoetherianRing_of_ringEquiv _
    (Scheme.restrictFunctorΓ.app (op U)).symm.commRingCatIsoToRingEquiv

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst✝ : IsNoetherianRing ↑Γ(X, U)
this : IsNoetherianRing ↑Γ(↑U, ⊤)
⊢ NoetherianSpace ↥↑U
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case hC
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝
      (((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))).comp
          C)
        x✝) =
    coeff m✝ (((map (algebraMap R x.asIdeal.ResidueField)).comp C) x✝)

pp: case hX
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝
      ((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))

Tactic:
·

Goal state after:
case hC
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝
      (((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))).comp
          C)
        x✝) =
    coeff m✝ (((map (algebraMap R x.asIdeal.ResidueField)).comp C) x✝)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (↑U ∩ Set.range ⇑f)

pp: case Kf
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ Set.range ⇑f

Tactic:
·

Goal state after:
case hK
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (↑U ∩ Set.range ⇑f)
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case refine_1
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ IsLocallyNoetherian X

pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ DiscreteTopology ↥X

Tactic:
·

Goal state after:
case refine_1
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ IsLocallyNoetherian X
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ NoetherianSpace ↑?m.46

pp: case hK.a
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ ?m.46

pp: X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ Set ↥X

Tactic:
·

Goal state after:
case hK.a
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ NoetherianSpace ↑?m.46
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: case hX
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝
      ((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))

Tactic:
·

Goal state after:
case hX
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝
      ((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ DiscreteTopology ↥X

Tactic:
·

Goal state after:
case refine_2
X : Scheme
𝒰 : X.OpenCover
H : ∀ (i : 𝒰.I₀), IsLocallyArtinian (𝒰.X i)
⊢ DiscreteTopology ↥X
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ ↑U

Tactic:
·

Goal state after:
case hK.a
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ ↑U
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case Kf
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ Set.range ⇑f

Tactic:
·

Goal state after:
case Kf
X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ ↑U ∩ Set.range ⇑f ⊆ Set.range ⇑f
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0 ↔ ∃ i, coeff i f ∉ x.asIdeal

Tactic:
·

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
⊢ (map (algebraMap R x.asIdeal.ResidueField)) f ≠ 0 ↔ ∃ i, coeff i f ∉ x.asIdeal
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑↑U ∩ ↑↑V))

pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ ↑↑V ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
·

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' (↑↑U ∩ ↑↑V))
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
this : ∀ {X : Scheme} [DiscreteTopology ↥X] [IsReduced X], Subsingleton ↥X → IsLocallyArtinian X
hX : ¬Subsingleton ↥X
⊢ IsLocallyArtinian X

pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
⊢ IsLocallyArtinian X

Tactic:
·

Goal state after:
case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
this : ∀ {X : Scheme} [DiscreteTopology ↥X] [IsReduced X], Subsingleton ↥X → IsLocallyArtinian X
hX : ¬Subsingleton ↥X
⊢ IsLocallyArtinian X
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (↑↑U ∩ (↑↑U ∩ ↑↑V))

pp: case Kf
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
·

Goal state after:
case hK
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (↑↑U ∩ (↑↑U ∩ ↑↑V))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ NoetherianSpace ↑?m.59

pp: case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ ?m.59

pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ Set ↥X

Tactic:
·

Goal state after:
case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ NoetherianSpace ↑?m.59
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ ↑↑U

Tactic:
·

Goal state after:
case hK.a
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ ↑↑U
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: case inl
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
h✝ : IsEmpty ↥X
⊢ IsLocallyArtinian X

pp: case inr
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
h✝ : Nonempty ↥X
⊢ IsLocallyArtinian X

Tactic:
·

Goal state after:
case inl
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
hX : Subsingleton ↥X
h✝ : IsEmpty ↥X
⊢ IsLocallyArtinian X
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case Kf
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
·

Goal state after:
case Kf
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ (↑↑U ∩ ↑↑V) ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ ↑↑V ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
·

Goal state after:
X : Scheme
inst✝ : IsLocallyNoetherian X
U V : ↑X.affineOpens
hInd : Topology.IsInducing ⇑(IsAffineOpen.fromSpec ⋯)
⊢ ↑↑U ∩ ↑↑V ⊆ Set.range ⇑(IsAffineOpen.fromSpec ⋯)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y],
    (∃ R, Y = Spec R) → id (IsLocallyNoetherian X)
hY : ¬∃ R, Y = Spec R
⊢ id (IsLocallyNoetherian X)

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
hY : ∃ R, Y = Spec R
⊢ id (IsLocallyNoetherian X)

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y],
    (∃ R, Y = Spec R) → id (IsLocallyNoetherian X)
hY : ¬∃ R, Y = Spec R
⊢ id (IsLocallyNoetherian X)
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: case refine_1
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
⊢ P Z

pp: case refine_2
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : MorphismProperty.universally (fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X) f
aK : Type u
y : Field aK
Z : Spec (of aK) ⟶ Y
W : Scheme
fst : W ⟶ X
snd : W ⟶ Spec (of aK)
h : IsPullback fst snd f Z
⊢ P W

Tactic:
·

Goal state after:
case refine_1
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : geometrically P f
Z W : Scheme
snd : Z ⟶ X
q : W ⟶ Y
fst : Z ⟶ W
h : IsPullback fst snd q f
x✝¹ : IsIntegral W
x✝ : Subsingleton ↥W
⊢ P Z
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
hY : ∃ R, Y = Spec R
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y],
    (∃ R, Y = Spec R) → (∃ S, X = Spec S) → id (IsLocallyNoetherian X)
hX : ¬∃ S, X = Spec S
⊢ id (IsLocallyNoetherian X)

pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
hY : ∃ R, Y = Spec R
hX : ∃ S, X = Spec S
⊢ id (IsLocallyNoetherian X)

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
hY : ∃ R, Y = Spec R
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y],
    (∃ R, Y = Spec R) → (∃ S, X = Spec S) → id (IsLocallyNoetherian X)
hX : ¬∃ S, X = Spec S
⊢ id (IsLocallyNoetherian X)
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: case refine_2
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : MorphismProperty.universally (fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X) f
aK : Type u
y : Field aK
Z : Spec (of aK) ⟶ Y
W : Scheme
fst : W ⟶ X
snd : W ⟶ Spec (of aK)
h : IsPullback fst snd f Z
⊢ P W

Tactic:
·

Goal state after:
case refine_2
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
hf : MorphismProperty.universally (fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X) f
aK : Type u
y : Field aK
Z : Spec (of aK) ⟶ Y
W : Scheme
fst : W ⟶ X
snd : W ⟶ Spec (of aK)
h : IsPullback fst snd f Z
⊢ P W
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mp
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ IsNoetherian X → ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))

pp: case mpr
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ (∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))) → IsNoetherian X

Tactic:
·

Goal state after:
case mp
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ IsNoetherian X → ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      pullback.fst f (Z.fromSpecResidueField (g y)))
    (Scheme.Hom.fiberToSpecResidueField snd y) f
    (Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y))

pp: case refine_2
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      Scheme.Hom.fiberToSpecResidueField f (g y) =
    Scheme.Hom.fiberToSpecResidueField snd y ≫ Spec.map (Scheme.Hom.residueFieldMap g y)

Tactic:
·

Goal state after:
case refine_1
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ IsPullback
    (pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      pullback.fst f (Z.fromSpecResidueField (g y)))
    (Scheme.Hom.fiberToSpecResidueField snd y) f
    (Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y))
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ (∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))) → IsNoetherian X

Tactic:
·

Goal state after:
case mpr
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ (∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))) → IsNoetherian X
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_2
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      Scheme.Hom.fiberToSpecResidueField f (g y) =
    Scheme.Hom.fiberToSpecResidueField snd y ≫ Spec.map (Scheme.Hom.residueFieldMap g y)

Tactic:
·

Goal state after:
case refine_2
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
y : ↥Y
⊢ pullback.map snd (Y.fromSpecResidueField y) f (Z.fromSpecResidueField (g y)) fst
        (Spec.map (Scheme.Hom.residueFieldMap g y)) g ⋯ ⋯ ≫
      Scheme.Hom.fiberToSpecResidueField f (g y) =
    Scheme.Hom.fiberToSpecResidueField snd y ≫ Spec.map (Scheme.Hom.residueFieldMap g y)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_2
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsLocallyNoetherian X

pp: case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ CompactSpace ↥X

Tactic:
·

Goal state after:
case mpr.convert_2
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsLocallyNoetherian X
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ CompactSpace ↥X

Tactic:
·

Goal state after:
case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ CompactSpace ↥X
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_1
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ pullback ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField))) (map (CommRingCat.ofHom (algebraMap R S)))

pp: case refine_2
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Spec ((Spec (CommRingCat.of R)).residueField p) ≅ Spec (CommRingCat.of p.asIdeal.ResidueField)

pp: case refine_3
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S))) ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
          ?refine_1 ≪≫ pullbackSpecIso R p.asIdeal.ResidueField S).hom ≫
      map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) =
    Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫ Iso.hom ?refine_2

Tactic:
·

Goal state after:
case refine_1
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ pullback ((Spec (CommRingCat.of R)).fromSpecResidueField p) (map (CommRingCat.ofHom (algebraMap R S))) ≅
    pullback (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField))) (map (CommRingCat.ofHom (algebraMap R S)))
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: case refine_1
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ IsPullback (p ≫ pullback.fst f (Y.fromSpecResidueField y)) snd f (Spec.map φ ≫ Y.fromSpecResidueField y)

pp: case refine_2
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ snd ≫ Spec.map φ = p ≫ Scheme.Hom.fiberToSpecResidueField f y

Tactic:
·

Goal state after:
case refine_1
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ IsPullback (p ≫ pullback.fst f (Y.fromSpecResidueField y)) snd f (Spec.map φ ≫ Y.fromSpecResidueField y)