mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).hom ≫ Y.ofRestrict ⋯ = f

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (isoRestrict f).inv ≫ f = Y.ofRestrict ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
i : op U' ⟶ op U
⊢ Y.presheaf.map i ≫ appLE f U V e = appLE f U' V ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Mono f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ app f U = appLE f U (f ⁻¹ᵁ U) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
V : Opens ↑↑Y
U : Opens ↑↑X
h : V = (opensFunctor f).obj U
⊢ IsIso (f.c.app (op V))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
e₁ : U = U'
e₂ : V = V'
P : {R S : CommRingCat} → (R ⟶ S) → Prop
⊢ P (appLE f U V e) ↔ P (appLE f U' V' ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom (f ≫ g).base)
⊢ h.functor.obj U = (opensFunctor g).obj ((opensFunctor f).obj U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
toLRSHom'✝¹ toLRSHom'✝ : X.Hom Y.toLocallyRingedSpace
h_base : { toLRSHom' := toLRSHom'✝¹ }.base = { toLRSHom' := toLRSHom'✝ }.base
h_app :
  ∀ (U : Y.Opens),
    { toLRSHom' := toLRSHom'✝¹ }.app U ≫ X.presheaf.map (eqToHom ⋯).op = { toLRSHom' := toLRSHom'✝ }.app U
U : TopologicalSpace.Opens ↥Y
⊢ (toLRSHom'✝¹.c ≫ Functor.whiskerRight (eqToHom ⋯) X.presheaf).app (op U) = toLRSHom'✝.c.app (op U)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
Z : PresheafedSpace C
g : Y ⟶ Z
hg : IsOpenImmersion g
U : Opens ↑↑X
⊢ IsIso ((f ≫ g).c.app (op (⋯.functor.obj U)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
h_base : f.base = g.base
h_app : ∀ (U : Y.Opens), app f U ≫ X.presheaf.map (eqToHom ⋯).op = app g U
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑X
⊢ op U = (Opens.map f.base).op.obj (op ((opensFunctor f).obj U))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
h : toLRSHom f = toLRSHom g
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → Y.Opens
⊢ ↑(f ⁻¹ᵁ iSup U) = ↑(⨆ i, f ⁻¹ᵁ U i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
⊢ (f ≫ g) x = g (f x)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) = invApp f (unop U) ≫ Y.presheaf.map ((opensFunctor f).op.map i)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ IsIso (invApp f U)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U : Opens ↑↑X
⊢ (Opens.map f.base).op.obj (op ((opensFunctor f).obj U)) = op U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : Y.Opens
W : X.Opens
e₁ : V ≤ g ⁻¹ᵁ U
e₂ : W ≤ f ⁻¹ᵁ V
⊢ appLE g U V e₁ ≫ appLE f V W e₂ = appLE (f ≫ g) U W ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ inv (invApp f U) = f.c.app (op ((opensFunctor f).obj U)) ≫ X.presheaf.map (eqToHom ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Z.Opens
V : X.Opens
e : V ≤ (f ≫ g) ⁻¹ᵁ U
⊢ appLE (f ≫ g) U V e = app g U ≫ appLE f (g ⁻¹ᵁ U) V e

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ f ⁻¹ᵁ U = g ⁻¹ᵁ U

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑X
⊢ invApp f U ≫ f.c.app (op ((opensFunctor f).obj U)) = X.presheaf.map (eqToHom ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
e : f = g
U : Y.Opens
⊢ app f U = app g U ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : Y.Opens
e : U = V
⊢ app f U = Y.presheaf.map (eqToHom ⋯).op ≫ app f V ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X = Y
U : Y.Opens
⊢ Γ(Y, U) = Γ(X, eqToHom e ⁻¹ᵁ U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X = Y
U : Y.Opens
⊢ app (eqToHom e) U = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
⊢ f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (homOfLE ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : X.Opens
⊢ app (inv f) U = X.presheaf.map (eqToHom ⋯).op ≫ inv (app f (inv f ⁻¹ᵁ U))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ appTop (inv f) = inv (appTop f)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑↑Y
hU : ↑U ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ f.c.app (op U) ≫ invApp f ((Opens.map f.base).obj U) = Y.presheaf.map (eqToHom ⋯).op

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
⊢ f.base = ofHom { toFun := g, continuous_toFun := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
⊢ (Opens.map f).obj (hf.functor.obj U) = U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
x : ↥X
⊢ IsLocalHom
    (CommRingCat.Hom.hom
      ({ base := ofHom { toFun := g, continuous_toFun := ⋯ },
            c := f.c ≫ (Presheaf.pushforwardEq ⋯ X.presheaf).hom }.stalkMap
        x))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
g : ↥X → ↥Y
h : ⇑f = g
⊢ f.copyBase g h = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCatᵒᵖ
⊢ Spec.map (𝟙 R).unop = 𝟙 (Spec (unop R))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ Spec.map (f ≫ g).unop = Spec.map f.unop ≫ Spec.map g.unop

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R S : CommRingCat
e : R = S
⊢ map (eqToHom e) = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
inst✝ : IsIso f
⊢ map (inv f) = inv (map f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
s : ↑Γ(Y, V)
⊢ X.basicOpen ((ConcreteCategory.hom (Hom.appLE f V U e)) s) = U ⊓ f ⁻¹ᵁ Y.basicOpen s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case e'_5.e_8.e_3
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ ⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) = unop (op (hf.functor.obj U))

Tactic:
simp only

Goal state after:
case e'_5.e_8.e_3
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
this : (Opens.map f).obj (hf.functor.obj U) = U
e_4✝ :
  Y.presheaf.obj (op (hf.functor.obj ((Opens.map f).obj (hf.functor.obj U)))) = Y.presheaf.obj (op (hf.functor.obj U))
⊢ ⋯.functor.obj ((Opens.map f).obj (hf.functor.obj U)) = hf.functor.obj U
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
⊢ X.basicOpen (f + g) ≤ X.basicOpen f ⊔ X.basicOpen g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ Codisjoint (X.zeroLocus s) ↑U

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
⊢ IsIso ((Y.ofRestrict hf).c.app (op (hf.functor.obj U)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s : Set ↑Γ(X, U)
⊢ X.zeroLocus ↑(Ideal.span s) = X.zeroLocus s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
Y : TopCat
f : Y ⟶ TopCat.of ↑↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(X.restrict h)
⊢ invApp (X.ofRestrict h) U = 𝟙 ((X.restrict h).presheaf.obj (op U))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
⊢ X.zeroLocus (s * t) = X.zeroLocus s ∪ X.zeroLocus t

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I J : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑(I * J) = X.zeroLocus ↑I ∪ X.zeroLocus ↑J

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
U : (Opens ↑↑Y)ᵒᵖ
⊢ U = op ((opensFunctor f).obj ((Opens.map f.base).obj (unop U)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↥X
this : (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f
⊢ x ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) ↔ x ∈ X.zeroLocus s ∪ (↑U)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↥X
⊢ x ∈ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) ↔ x ∈ X.zeroLocus s ∪ (↑U)ᶜ

Tactic:
suffices (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → (∀ f ∈ s, x ∉ X.basicOpen f) by
    simpa [or_iff_not_imp_right]

Goal state after:
X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
x : ↥X
⊢ (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → ∀ f ∈ s, x ∉ X.basicOpen f
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
⊢ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) = X.zeroLocus s ∪ (↑U)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
this✝ : ∀ (U : (Opens ↑↑Y)ᵒᵖ), IsIso (f.c.app U)
this : IsIso f.c
x : ↑↑Y
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom f.base)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
i : U = V
s : Set ↑Γ(X, V)
⊢ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (eqToHom i).op)) '' s) = X.zeroLocus s

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
h' : Epi f.base
⊢ IsIso f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
s t : Set ↑Γ(X, U)
h : s ⊆ t
⊢ X.zeroLocus t ⊆ X.zeroLocus s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set ↑Γ(Y, U)
⊢ ⇑f ⁻¹' Y.zeroLocus s = X.zeroLocus (⇑(CommRingCat.Hom.hom (Hom.app f U)) '' s)

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : HasColimits C
x : ↑↑X
⊢ IsIso (Hom.stalkMap f x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
x✝ : x ∈ U
⊢ x ∈ X.basicOpen 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ X.zeroLocus Set.univ = (↑U)ᶜ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
f : ι → Set ↑Γ(X, U)
⊢ X.zeroLocus (⋃ i, f i) = ⋂ i, X.zeroLocus (f i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : ↑Γ(X, U)
hx : x ∈ X.basicOpen f
hn : f ^ 0 ∈ I
⊢ f ∈ I

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
p : PrimeSpectrum ↑R
inst✝ : Algebra ↑R ↑S
y :
  ↑(((TopCat.Presheaf.pushforward CommRingCat (Spec.topMap (CommRingCat.ofHom (algebraMap ↑R ↑S)))).obj
          (structureSheaf ↑S).obj).stalk
      p)
⊢ ∃ x, x.2 • y = (toPushforwardStalkAlgHom R S p) x.1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
I : Ideal ↑Γ(X, U)
⊢ X.zeroLocus ↑I.radical = X.zeroLocus ↑I

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U : (Opens ↑↑X)ᵒᵖ
⊢ (Opens.map g.base).op.obj (op (⋯.functor.obj (unop U))) =
    ⋯.functor.op.obj ((Opens.map (pullback.fst f.base g.base)).op.obj U)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
x : ↥(Spec R)
this : IsUnit ((algebraMap ↑R ↑((structurePresheafInCommRingCat ↑R).stalk x)) f) ↔ f ∉ x.asIdeal
⊢ IsUnit
      ((ConcreteCategory.hom ((Spec R).presheaf.germ ⊤ x _root_.trivial))
        ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f)) ↔
    x ∈ PrimeSpectrum.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑R
⊢ (Spec R).basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) f) = PrimeSpectrum.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
f : ↑Γ(Spec R, ⊤)
⊢ (Spec R).basicOpen f = PrimeSpectrum.basicOpen ((ConcreteCategory.hom (Scheme.ΓSpecIso R).hom) f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Γ(Spec Γ(X, V), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (eqToHom h).op) ⁻¹ᵁ W)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
⊢ ∀ ⦃X_1 Y_1 : (Opens ↑↑X)ᵒᵖ⦄ (f_1 : X_1 ⟶ Y_1),
    X.presheaf.map f_1 ≫ invApp f (unop Y_1) ≫ g.c.app (op (⋯.functor.obj (unop Y_1))) ≫ Y.presheaf.map (eqToHom ⋯) =
      (invApp f (unop X_1) ≫ g.c.app (op (⋯.functor.obj (unop X_1))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
        ((TopCat.Presheaf.pushforward C (pullback.fst f.base g.base)).obj (Y.restrict ⋯).presheaf).map f_1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (eqToHom h).op)) W = eqToHom ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) s)
n : ℕ
hf : s ^ n * f = 0
⊢ IsUnit ((ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) (s ^ n))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : Opens ↥X
x : ↥U
f s : ↑Γ(X, U)
hx : ↑x ∈ X.basicOpen s
n : ℕ
hf : s ^ n * f = 0
⊢ (ConcreteCategory.hom (X.presheaf.germ U ↑x ⋯)) f = 0

Tactic:
by

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
⊢ pullbackConeOfLeftFst f g ≫ f = Y.ofRestrict ⋯ ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x) = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
e : X ≅ Y
y : ↥Y
⊢ e.hom (e.inv y) = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑R
x : ↥(Spec R)
this : (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s
⊢ x ∈ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) ↔ x ∈ PrimeSpectrum.zeroLocus s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑R
⊢ (Spec R).zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) '' s) = PrimeSpectrum.zeroLocus s

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: R : CommRingCat
s : Set ↑Γ(Spec R, ⊤)
⊢ (Spec R).zeroLocus s = PrimeSpectrum.zeroLocus (⇑(ConcreteCategory.hom (Scheme.ΓSpecIso R).inv) ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↥Y
⊢ e.hom (e.inv y) = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↥Y
z : ↑(Y.presheaf.stalk (e.hom (e.inv y)))
⊢ e.hom (e.inv y) = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x) = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↥X
y : ↑(X.presheaf.stalk (e.inv (e.hom x)))
⊢ e.inv (e.hom x) = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ (Y.presheaf.stalkCongr ⋯).hom ≫ (Arrow.mk (stalkMap f y)).hom =
    (Arrow.mk (stalkMap f x)).hom ≫ (X.presheaf.stalkCongr ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
x : ↑X.toTopCat
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ : x ∈ Set.range ⇑(ConcreteCategory.hom f.base)
h₂ : IsOpenImmersion f
⊢ X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R)

Tactic:
apply LocallyRingedSpace.isoOfSheafedSpaceIso

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
x : ↑X.toTopCat
R : CommRingCat
f : Spec.toLocallyRingedSpace.obj (op R) ⟶ X
h₁ : x ∈ Set.range ⇑(ConcreteCategory.hom f.base)
h₂ : IsOpenImmersion f
⊢ (X.restrict ⋯).toSheafedSpace ≅ (Spec.toLocallyRingedSpace.obj (op R)).toSheafedSpace
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : LocallyRingedSpace
h : ∀ (x : ↑X.toTopCat), ∃ R f, x ∈ Set.range ⇑(ConcreteCategory.hom f.base) ∧ IsOpenImmersion f
⊢ ∀ (x : ↑X.toTopCat), ∃ U R, Nonempty (X.restrict ⋯ ≅ Spec.toLocallyRingedSpace.obj (op R))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
⊢ (opensFunctor f).IsCocontinuous (Opens.grothendieckTopology ↥X) (Opens.grothendieckTopology ↥Y)

Tactic:
by

Goal state after: