internlm/Lean-Github huggingface dataset:
Theorem: PolynomialMap.exists_lift'
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
have hAB : A ≤ A ⊔ Algebra.adjoin R ({s} : Finset S) := le_sup_left
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Theorem: PolynomialMap.exists_lift'
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ A ⊔ Algebra.adjoin R ↑{s}
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
rw [← hgen] at hAB
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Theorem: PolynomialMap.exists_lift'
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
choose p hp using exists_lift_of_le_rTensor_range M _ hAB t ht
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Theorem: PolynomialMap.exists_lift'
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
have : s ∈ (φ R gen).range  := by
  rw [hgen]
  apply Algebra.subset_adjoin
  simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
  exact Or.inr (Algebra.subset_adjoin rfl)
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
this : s ∈ (PolynomialMap.φ R gen).range
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Theorem: PolynomialMap.exists_lift'
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
this : s ∈ (PolynomialMap.φ R gen).range
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
choose q hq using this
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
q : MvPolynomial (Fin gen.card) R
hq : (PolynomialMap.φ R gen).toRingHom q = s
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Theorem: PolynomialMap.exists_lift'
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
q : MvPolynomial (Fin gen.card) R
hq : (PolynomialMap.φ R gen).toRingHom q = s
⊢ ∃ n ψ p q, (LinearMap.rTensor M ψ.toLinearMap) p = t ∧ ψ q = s
Tactic:
use gen.card, φ R gen, p, q, hp, hq
Proof state after:
no goals
Theorem: PolynomialMap.exists_lift'
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ (PolynomialMap.φ R gen).range
Tactic:
rw [hgen]
Proof state after:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ A ⊔ Algebra.adjoin R ↑{s}
Theorem: PolynomialMap.exists_lift'
Proof state before:
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ A ⊔ Algebra.adjoin R ↑{s}
Tactic:
apply Algebra.subset_adjoin
Proof state after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ ↑A ⊔ ↑(Algebra.adjoin R ↑{s})
Theorem: PolynomialMap.exists_lift'
Proof state before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ ↑A ⊔ ↑(Algebra.adjoin R ↑{s})
Tactic:
simp only [Finset.coe_singleton, Set.sup_eq_union, Set.mem_union, SetLike.mem_coe]
Proof state after:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ A ∨ s ∈ Algebra.adjoin R {s}
Theorem: PolynomialMap.exists_lift'
Proof state before:
case a
R : Type u
inst✝⁶ : CommRing R
M : Type u_1
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommGroup N
inst✝² : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : S
A : Subalgebra R S
hA : A.FG
ht : t ∈ range (LinearMap.rTensor M A.val.toLinearMap)
hB : (A ⊔ Algebra.adjoin R ↑{s}).FG
gen : Finset S
hgen : (PolynomialMap.φ R gen).range = A ⊔ Algebra.adjoin R ↑{s}
hAB : A ≤ (PolynomialMap.φ R gen).range
p : MvPolynomial (Fin gen.card) R ⊗[R] M
hp : (LinearMap.rTensor M (PolynomialMap.φ R gen).toLinearMap) p = t
⊢ s ∈ A ∨ s ∈ Algebra.adjoin R {s}
Tactic:
exact Or.inr (Algebra.subset_adjoin rfl)
Proof state after:
no goals
Theorem: PolynomialMap.toFun_eq_toFun'
Proof state before:
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ f.toFun S = f.toFun' S
Tactic:
ext t
Proof state after:
case h
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ f.toFun S t = f.toFun' S t
Theorem: PolynomialMap.toFun_eq_toFun'
Proof state before:
case h
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
⊢ f.toFun S t = f.toFun' S t
Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
Proof state after:
case h.intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ f.toFun S t = f.toFun' S t
Theorem: PolynomialMap.toFun_eq_toFun'
Proof state before:
case h.intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ f.toFun S t = f.toFun' S t
Tactic:
simp only [f.toFun_eq_toFunLifted_apply ha, toFunLifted, f.isCompat_apply']
Proof state after:
case h.intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ f.toFun' S ((LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p) = f.toFun' S t
Theorem: PolynomialMap.toFun_eq_toFun'
Proof state before:
case h.intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S✝ : Type v
inst✝³ : CommRing S✝
inst✝² : Algebra R S✝
S : Type u
inst✝¹ : CommRing S
inst✝ : Algebra R S
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ f.toFun' S ((LinearMap.rTensor M (PolynomialMap.φ R s).toLinearMap) p) = f.toFun' S t
Tactic:
exact congr_arg _ ha
Proof state after:
no goals
Theorem: PolynomialMap.isCompat_apply
Proof state before:
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
obtain ⟨⟨s, p⟩, ha⟩ := π_surjective t
Proof state after:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Theorem: PolynomialMap.isCompat_apply
Proof state before:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
let s' := s.image h
Proof state after:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Theorem: PolynomialMap.isCompat_apply
Proof state before:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
let h' : (φ R s).range →ₐ[R] (φ R s').range :=
  (h.comp (Subalgebra.val _)).codRestrict (φ R s').range (by
  rintro ⟨x, hx⟩
  simp only [φ_range] at hx ⊢
  simp only [AlgHom.coe_comp, Subalgebra.coe_val, Function.comp_apply, Finset.coe_image,
    Algebra.adjoin_image, s']
  exact ⟨x, hx, rfl⟩)
Proof state after:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(PolynomialMap.φ R s).range →ₐ[R] ↥(PolynomialMap.φ R s').range :=
  (h.comp (PolynomialMap.φ R s).range.val).codRestrict (PolynomialMap.φ R s').range ⋯
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Theorem: PolynomialMap.isCompat_apply
Proof state before:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(PolynomialMap.φ R s).range →ₐ[R] ↥(PolynomialMap.φ R s').range :=
  (h.comp (PolynomialMap.φ R s).range.val).codRestrict (PolynomialMap.φ R s').range ⋯
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
let j : Fin s.card → Fin s'.card :=
  (s'.equivFin) ∘ (fun ⟨x, hx⟩ ↦ ⟨h x, Finset.mem_image_of_mem h hx⟩) ∘ (s.equivFin).symm
Proof state after:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(PolynomialMap.φ R s).range →ₐ[R] ↥(PolynomialMap.φ R s').range :=
  (h.comp (PolynomialMap.φ R s).range.val).codRestrict (PolynomialMap.φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Theorem: PolynomialMap.isCompat_apply
Proof state before:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(PolynomialMap.φ R s).range →ₐ[R] ↥(PolynomialMap.φ R s').range :=
  (h.comp (PolynomialMap.φ R s).range.val).codRestrict (PolynomialMap.φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)
Tactic:
have eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s) := by
  ext p
  simp only [φ, AlgHom.comp_apply, aeval_rename, comp_aeval]
  congr
  ext n
  simp only [Function.comp_apply, Equiv.symm_apply_apply, j]
Proof state after:
case intro.mk
R : Type u
inst✝⁸ : CommRing R
M : Type u_1
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
f✝ f : M →ₚ[R] N
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
T : Type w
inst✝¹ : CommRing T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : PolynomialMap.π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(PolynomialMap.φ R s).range →ₐ[R] ↥(PolynomialMap.φ R s').range :=
  (h.comp (PolynomialMap.φ R s).range.val).codRestrict (PolynomialMap.φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (PolynomialMap.φ R s').comp (rename j) = h.comp (PolynomialMap.φ R s)
⊢ (LinearMap.rTensor N h.toLinearMap) (f.toFun S t) = f.toFun T ((LinearMap.rTensor M h.toLinearMap) t)