mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: case hX
n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : σ
⊢ (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom (MvPolynomial.X i✝) =
    ((algebraMap P.Ring S).comp e.toRingEquiv.toRingHom) (MvPolynomial.X i✝)

Tactic:
·

Goal state after:
case hX
n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
i✝ : σ
⊢ (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom (MvPolynomial.X i✝) =
    ((algebraMap P.Ring S).comp e.toRingEquiv.toRingHom) (MvPolynomial.X i✝)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : Unit
⊢ D.basis (Sum.inl r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩

pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ D.basis (Sum.inr r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
·

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : Unit
⊢ D.basis (Sum.inl r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inl r), ⋯⟩
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ D.basis (Sum.inr r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩

Tactic:
·

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
r : σ
⊢ D.basis (Sum.inr r) = Extension.Cotangent.mk ⟨D.pres.relation (Sum.inr r), ⋯⟩
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t).IsHomogeneous 1

pp: case refine_2.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) t) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i - X i)

Tactic:
·

Goal state after:
case refine_2.refine_1
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ ((MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t).IsHomogeneous 1
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: case refine_2.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) t) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i - X i)

Tactic:
·

Goal state after:
case refine_2.refine_2
R : Type u_1
inst✝⁴ : CommRing R
A : Type u
B : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : CommRing B
inst✝ : Algebra A B
D : DescentAux A B
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
hinj : Function.Injective ⇑(MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
t : MvPolynomial D.rels (MvPolynomial D.vars ↥(subalgebra R D))
ht : (MvPolynomial.map (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))) t = D.q i
⊢ (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A))
      ((eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) t) =
    (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i - X i)
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

pp: case inr
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Nontrivial S
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
·

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inl
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

pp: case inr
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Nontrivial S
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
·

Goal state after:
case inl
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ Ideal.span (Set.range fun x ↦ 1) = (ofSurjective (fun i ↦ 0) ⋯).ker

Tactic:
by simpa using! (RingHom.ker_eq_top_of_subsingleton _).symm

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ (∀ (x : ↥X),
      ∃ U V,
        ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).IsStandardSmooth) ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : IsAffineOpen U),
          ∃ V,
            ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

pp: case hQ
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

pp: case hQi
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
·

Goal state after:
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ (∀ (x : ↥X),
      ∃ U V,
        ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).IsStandardSmooth) ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : IsAffineOpen U),
          ∃ V,
            ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case hQ
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

pp: case hQi
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
·

Goal state after:
case hQ
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case hQi
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
·

Goal state after:
case hQi
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case hQl
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n

pp: case hQa
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n

pp: case h
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    SmoothOfRelativeDimension n f ↔
      ∀ (x : ↥X),
        ∃ U V,
          ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
            IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
·

Goal state after:
case hQl
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case hQa
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n

pp: case h
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    SmoothOfRelativeDimension n f ↔
      ∀ (x : ↥X),
        ∃ U V,
          ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
            IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
·

Goal state after:
case hQa
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderCompositionWithLocalizationAway fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case h
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    SmoothOfRelativeDimension n f ↔
      ∀ (x : ↥X),
        ∃ U V,
          ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
            IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))

Tactic:
·

Goal state after:
case h
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    SmoothOfRelativeDimension n f ↔
      ∀ (x : ↥X),
        ∃ U V,
          ∃ (_ : x ∈ ↑V) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
            IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)

pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q) ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
·

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case hC
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := ⋯
x✝ : k
⊢ ↑(((↑((renameEquiv k d).trans
                (H.aevalEquiv.trans
                  ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)))).comp
          C)
        x✝) =
    ↑(((↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp C) x✝)

Tactic:
simp [d]

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case hX
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := ⋯
i✝ : { j // j ≠ i }
⊢ ↑(↑((renameEquiv k d).trans
            (H.aevalEquiv.trans
              ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯)))
        (X i✝)) =
    ↑(↑(aeval fun j ↦ ⟨a ↑j, ⋯⟩) (X i✝))

Tactic:
simp [d]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q) ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
·

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝¹ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := ⋯
p : Ideal ↑Γ(Y, U) := ⋯
q : Ideal ↑Γ(X, V) := ⋯
this✝ : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := ⋯
⊢ Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q) ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case inr
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
this : ∀ (q₁ q₂ : MvPolynomial ι k), F = q₁ * q₂ → (aeval a) q₁ = 0 → IsUnit q₁ ∨ IsUnit q₂
h₁ : ¬(aeval a) q₁ = 0
⊢ IsUnit q₁ ∨ IsUnit q₂

pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : (aeval a) q₁ = 0
⊢ IsUnit q₁ ∨ IsUnit q₂

Tactic:
·

Goal state after:
case inr
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
this : ∀ (q₁ q₂ : MvPolynomial ι k), F = q₁ * q₂ → (aeval a) q₁ = 0 → IsUnit q₁ ∨ IsUnit q₂
h₁ : ¬(aeval a) q₁ = 0
⊢ IsUnit q₁ ∨ IsUnit q₂