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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : Module.Free R A
inst✝¹ : Module.Finite R A
f : A
I : Ideal R
inst✝ : I.IsPrime
⊢ IsNilpotent ((algebraMap A (A ⊗[R] I.ResidueField)) f) ↔
    ∀ i < Module.finrank R A, (LinearMap.charpoly ((Algebra.lmul R A) f)).coeff i ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
q : PrimeSpectrum A
H : IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] (comap (algebraMap R A) q).asIdeal.ResidueField)) f)
hqg : s ⊆ ↑q.asIdeal
hqf : f ∉ q.asIdeal
⊢ Ideal.span s ≤ RingHom.ker (algebraMap A q.asIdeal.ResidueField)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
B' : Subalgebra K B
hB : B'.FG
f : A ⊗[K] ↥B'
hU : IsOpen ↑(basicOpen ((Algebra.TensorProduct.map (AlgHom.id A A) B'.val).toRingHom f))
this : Algebra.FinitePresentation K ↥B'
x : PrimeSpectrum A
ψ : A ⊗[K] ↥B' ⊗[A] x.asIdeal.ResidueField →ₐ[A] A ⊗[K] B ⊗[A] x.asIdeal.ResidueField :=
  Algebra.TensorProduct.map (Algebra.TensorProduct.map (AlgHom.id A A) B'.val) (AlgHom.id A x.asIdeal.ResidueField)
hψeq :
  ψ =
    (↑(Algebra.TensorProduct.comm A x.asIdeal.ResidueField (A ⊗[K] B))).comp
      ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField B).symm).comp
        ((Algebra.TensorProduct.map (AlgHom.id A x.asIdeal.ResidueField) B'.val).comp
          ((↑(Algebra.TensorProduct.cancelBaseChange K A A x.asIdeal.ResidueField ↥B')).comp
            ↑(Algebra.TensorProduct.comm A (A ⊗[K] ↥B') x.asIdeal.ResidueField))))
⊢ Injective ⇑ψ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Chevalley

Goal state before:
pp: K : Type u_3
A : Type u_4
B : Type u_5
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra K A
inst✝ : Algebra K B
⊢ IsOpenMap (comap (algebraMap A (A ⊗[K] B)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun s ↦ algebraMap R (Localization.Away s)
suitableN : R → Set ℕ := fun s ↦ {n | ∀ (m : ℕ), n ≤ m → Ideal.map (floc s) (I n) = Ideal.map (floc s) (I m)}
minN : R → ℕ := fun s ↦ sInf (suitableN s)
⊢ ∀ (s : ↥S), minN ↑s ∈ suitableN ↑s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
a : A
ha : a ∈ s
⊢ (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) { asIdeal := q, isPrime := hq } ∈ zeroLocus s

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
q : Ideal ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)
hq : q.IsPrime
hfq : (Ideal.Quotient.mk (Ideal.span s)) f ⊗ₜ[R] 1 ∉ q
this : ∀ a ∈ s, (Ideal.Quotient.mk (Ideal.span s)) a ⊗ₜ[R] 1 ∈ q
⊢ comap (algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) { asIdeal := q, isPrime := hq } ∉ zeroLocus {f}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : Type u
inst✝ : CommRing R
S : Finset R
hS : Ideal.span ↑S = ⊤
hN : ∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)
⊢ IsNoetherianRing R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
s : Set A
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) ↔
    ¬IsNilpotent ((algebraMap A ((A ⧸ Ideal.span s) ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
rw [← IsNilpotent.map_iff e.injective, AlgEquiv.commutes,
    ← mem_image_comap_zeroLocus_sdiff f ∅ x, zeroLocus_empty, ← Set.compl_eq_univ_sdiff,
    basicOpen_eq_zeroLocus_compl]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ x ∈ comap (algebraMap R A) '' ↑(basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
ι : Sort u_1
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
hS' : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsLocallyNoetherian X

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
A : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing A
inst✝² : Algebra R A
f : A
s : Set A
inst✝¹ : Module.Finite R (A ⧸ Ideal.span s)
inst✝ : Module.Free R (A ⧸ Ideal.span s)
⊢ ∃ t, comap (algebraMap R A) '' (zeroLocus s \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
x : PrimeSpectrum R
⊢ x ∈ comap C '' ↑(basicOpen f) ↔ ∃ i, f.coeff i ∉ x.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ comap C '' ↑(basicOpen f) = (zeroLocus (Set.range f.coeff))ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ IsOpenMap (comap C)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ Function.Surjective (comap C)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ ∃ t, comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : comap C '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
x✝ : ↑↑t
⊢ IsCompact (zeroLocus {↑x✝})ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ IsCompact (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ IsOpen (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsNoetherianRing ↑R
⊢ NoetherianSpace ↥(Spec R)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst✝ : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
⊢ IsLocallyConstructible (⇑f '' s)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsNoetherianRing ↑R
⊢ ⨆ i, ↑⟨⊤, ⋯⟩ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
h : topologicalKrullDim ↥X ≤ 0
U : ↑X.affineOpens
⊢ IsArtinianRing ↑Γ(X, ↑U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsLocallyArtinian X
⊢ DiscreteTopology ↥X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X Z : Scheme
inst✝¹ : IsLocallyNoetherian X
f : Z ⟶ X
inst✝ : IsOpenImmersion f
⊢ QuasiCompact f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
H : ∀ (i : ι), IsArtinianRing ↑Γ(X, U i)
⊢ ∀ (i : ι), IsLocallyArtinian (Spec Γ(X, U i))

Tactic:
by

Goal state after:
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) ↔ ∃ i, coeff i f ∉ x.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
ι : Type u_1
U : ι → X.Opens
hU : TopologicalSpace.IsOpenCover U
hU' : ∀ (i : ι), IsAffineOpen (U i)
⊢ IsLocallyArtinian X ↔ ∀ (i : ι), IsArtinianRing ↑Γ(X, U i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
⊢ comap C '' ↑(basicOpen f) = (zeroLocus (Set.range fun m ↦ coeff m f))ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: 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
⊢ ⨆ x, { carrier := {x}, is_open' := ⋯ } = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
⊢ IsOpenMap (comap C)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
⊢ Function.Surjective (comap C)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
⊢ IsLocallyArtinian X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X : Scheme
⊢ IsArtinianScheme X ↔ IsNoetherian X ∧ DiscreteTopology ↥X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: R : CommRingCat
⊢ IsArtinianScheme (Spec R) ↔ IsArtinianRing ↑R

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
⊢ QuasiSeparatedSpace ↥X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFiniteType f
inst✝ : IsLocallyNoetherian Y
⊢ IsLocallyNoetherian X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
⊢ geometrically P = MorphismProperty.universally fun X Y x ↦ IsIntegral Y → Subsingleton ↥Y → P X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X✝ : Scheme
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsLocallyNoetherian Y
inst✝ : LocallyOfFiniteType f
⊢ LocallyOfFinitePresentation f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P Q : ObjectProperty Scheme
⊢ geometrically (P ⊓ Q) = geometrically P ⊓ geometrically Q

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
⊢ (geometrically P).IsStableUnderBaseChange

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X✝ Y✝ 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
⊢ Y.fromSpecResidueField y ≫ g = Spec.map (Scheme.Hom.residueFieldMap g y) ≫ Z.fromSpecResidueField (g y)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral ↑(U i) → Subsingleton ↥↑(U i) → P ↑(f ⁻¹ᵁ U i)
x✝² : IsIntegral Y
x✝¹ : Subsingleton ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
z : ↥Y
x✝ : z ∈ ⊤
⊢ z ∈ U i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
X Y : Scheme
f : X ⟶ Y
ι : Type u
U : ι → Y.Opens
hU : TopologicalSpace.IsOpenCover U
H : ∀ (i : ι), IsIntegral ↑(U i) → Subsingleton ↥↑(U i) → P ↑(f ⁻¹ᵁ U i)
x✝¹ : IsIntegral Y
x✝ : Subsingleton ↥Y
y : ↥Y
i : ι
hy : y ∈ U i
heq : U i = ⊤
e : ↑(U i) ≅ Y := Y.isoOfEq heq ≪≫ Y.topIso
⊢ f ⁻¹ᵁ U i = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: 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 ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField snd y) (Scheme.Hom.fiberToSpecResidueField f (g y))
    (Spec.map (Scheme.Hom.residueFieldMap g y))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
inst✝ : P.IsClosedUnderIsomorphisms
⊢ IsZariskiLocalAtTarget (geometrically P)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst✝ : P.IsClosedUnderIsomorphisms
⊢ geometrically P f ↔ ∀ (K : Type u) [inst : Field K] (y : Spec (of K) ⟶ Y), P (pullback f y)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
        map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R)) p.asIdeal.ResidueField))) ≫
      𝟙 (Spec (CommRingCat.of R)) =
    map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
      map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: 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 ((Scheme.SpecToEquivOfField K Y).symm ⟨y, φ⟩)
⊢ fst ≫ f = (snd ≫ Spec.map φ) ≫ Y.fromSpecResidueField y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ map (CommRingCat.ofHom (algebraMap R S)) ≫ 𝟙 (Spec (CommRingCat.of R)) =
    𝟙 (Spec (CommRingCat.of S)) ≫ map (CommRingCat.ofHom (algebraMap R S))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
⊢ geometrically P f ↔ ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
hf : geometrically P f
⊢ P X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝ : CommRing R
f : X ⟶ Spec (of R)
⊢ geometrically P f ↔
    ∀ ⦃K : Type u⦄ [inst : Field K] [inst_1 : Algebra R K] ⦃Y : Scheme⦄ (fst : Y ⟶ X) (snd : Y ⟶ Spec (of K)),
      IsPullback fst snd f (Spec.map (ofHom (algebraMap R K))) → P Y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

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

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Arrow.mk (Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p) ≅
    Arrow.mk (map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
y : ↥Y
⊢ Set.range ⇑(fiberι f y) = ⇑f ⁻¹' {y}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ X.fromSpecResidueField x ≫ f = Spec.map (residueFieldMap f x) ≫ Y.fromSpecResidueField (f x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
y : ↥(Spec (X.residueField x))
⊢ (fiberι f (f x)) ((asFiberHom f x) y) = (fiberι f (f x)) (asFiber f x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Set.range ⇑(asFiberHom f x) = {asFiber f x}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: X : Scheme
P : ObjectProperty Scheme
R : Type u
inst✝¹ : CommRing R
f : X ⟶ Spec (of R)
inst✝ : P.IsClosedUnderIsomorphisms
⊢ geometrically P f ↔
    ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra R K], P (pullback f (Spec.map (ofHom (algebraMap R K))))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ IsNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.I₀), NoetherianSpace ↑(Set.range ⇑(𝒰.f i))
⊢ NoetherianSpace ↑(⋃ i, Set.range ⇑(𝒰.f i))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
⊢ IsAffine (𝒰.X i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsNoetherian X
⊢ NoetherianSpace ↥X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
this : IsNoetherianRing ↑(CommRingCat.of R)
⊢ IsNoetherian (Spec (CommRingCat.of R))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherian (Spec (CommRingCat.of R))

Tactic:
suffices IsNoetherianRing (CommRingCat.of R) by infer_instance

Goal state after:
X : Scheme
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherianRing ↑(CommRingCat.of R)
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
⊢ IsNoetherian (Spec (CommRingCat.of R))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
x : ↥X
⊢ x ∈ ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
inst✝ : IsLocallyNoetherian X
x : ↥X
⊢ IsNoetherianRing ↑(X.presheaf.stalk x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: R : CommRingCat
⊢ IsNoetherian (Spec R) ↔ IsNoetherianRing ↑R

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : IsIso f
⊢ Scheme.Hom.ker f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
⊢ IsDominant f

Tactic:
rw [isDominant_iff, DenseRange, dense_iff_closure_eq, ← Scheme.Hom.support_ker,
    f.ker_eq_bot, Scheme.IdealSheafData.support_bot, TopologicalSpace.Closeds.coe_top]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
⊢ IsDominant f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: ⊢ @GeometricallyReduced = geometrically IsReduced

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y Z S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : IsSchemeTheoreticallyDominant g
⊢ IsSchemeTheoreticallyDominant (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsDominant f
inst✝ : IsReduced Y
⊢ IsSchemeTheoreticallyDominant f

Tactic:
by

Goal state after: