internlm/Lean-Github huggingface dataset:
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ hI.isDPMorphism hK h
Tactic:
rw [← hcomp]
Proof state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ hI.isDPMorphism hK (g.comp f)
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ hI.isDPMorphism hK (g.comp f)
Tactic:
constructor
Proof state after:
case left
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map (g.comp f) I ≤ K

case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n ((g.comp f) a) = (g.comp f) (hI.dpow n a)
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
case left
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map (g.comp f) I ≤ K
Tactic:
apply le_trans _ hg.1
Proof state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map (g.comp f) I ≤ Ideal.map g J
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map (g.comp f) I ≤ Ideal.map g J
Tactic:
rw [← Ideal.map_map]
Proof state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map g (Ideal.map f I) ≤ Ideal.map g J
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ Ideal.map g (Ideal.map f I) ≤ Ideal.map g J
Tactic:
exact Ideal.map_mono hf.1
Proof state after:
no goals
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
⊢ ∀ (n : ℕ), ∀ a ∈ I, hK.dpow n ((g.comp f) a) = (g.comp f) (hI.dpow n a)
Tactic:
intro n a ha
Proof state after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n ((g.comp f) a) = (g.comp f) (hI.dpow n a)
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n ((g.comp f) a) = (g.comp f) (hI.dpow n a)
Tactic:
simp only [RingHom.coe_comp, Function.comp_apply]
Proof state after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n (g (f a)) = g (f (hI.dpow n a))
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n (g (f a)) = g (f (hI.dpow n a))
Tactic:
rw [← hf.2 n a ha]
Proof state after:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n (g (f a)) = g (hJ.dpow n (f a))
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
case right
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ hK.dpow n (g (f a)) = g (hJ.dpow n (f a))
Tactic:
rw [hg.2]
Proof state after:
case right.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ J
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
case right.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ J
Tactic:
apply hf.1
Proof state after:
case right.a.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ Ideal.map f I
Theorem: DividedPowers.isDPMorphism.comp
Proof state before:
case right.a.a
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
hg : hJ.isDPMorphism hK g
hf : hI.isDPMorphism hJ f
n : ℕ
a : A
ha : a ∈ I
⊢ f a ∈ Ideal.map f I
Tactic:
exact Ideal.mem_map_of_mem f ha
Proof state after:
no goals
Theorem: DividedPowers.isDPMorphism_on_span
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
⊢ hI.isDPMorphism hJ f
Tactic:
suffices h : I.map f ≤ J by
  apply And.intro h
  let dp_f := dpMorphismFromGens hI hJ hS h hdp
  intro n a ha
  rw [← dpMorphismFromGens_coe hI hJ hS h hdp, dp_f.dpow_comp n a ha]
Proof state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
⊢ Ideal.map f I ≤ J
Theorem: DividedPowers.isDPMorphism_on_span
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
⊢ Ideal.map f I ≤ J
Tactic:
rw [hS, Ideal.map_span, Ideal.span_le]
Proof state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
⊢ ⇑f '' S ⊆ ↑J
Theorem: DividedPowers.isDPMorphism_on_span
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
⊢ ⇑f '' S ⊆ ↑J
Tactic:
rintro b ⟨a, has, rfl⟩
Proof state after:
case intro.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
a : A
has : a ∈ S
⊢ f a ∈ ↑J
Theorem: DividedPowers.isDPMorphism_on_span
Proof state before:
case intro.intro
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
a : A
has : a ∈ S
⊢ f a ∈ ↑J
Tactic:
exact hS' a has
Proof state after:
no goals
Theorem: DividedPowers.isDPMorphism_on_span
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : Ideal.map f I ≤ J
⊢ hI.isDPMorphism hJ f
Tactic:
apply And.intro h
Proof state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : Ideal.map f I ≤ J
⊢ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
Theorem: DividedPowers.isDPMorphism_on_span
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : Ideal.map f I ≤ J
⊢ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
Tactic:
let dp_f := dpMorphismFromGens hI hJ hS h hdp
Proof state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : Ideal.map f I ≤ J
dp_f : hI.dpMorphism hJ := hI.dpMorphismFromGens hJ hS h hdp
⊢ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
Theorem: DividedPowers.isDPMorphism_on_span
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : Ideal.map f I ≤ J
dp_f : hI.dpMorphism hJ := hI.dpMorphismFromGens hJ hS h hdp
⊢ ∀ (n : ℕ), ∀ a ∈ I, hJ.dpow n (f a) = f (hI.dpow n a)
Tactic:
intro n a ha
Proof state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : Ideal.map f I ≤ J
dp_f : hI.dpMorphism hJ := hI.dpMorphismFromGens hJ hS h hdp
n : ℕ
a : A
ha : a ∈ I
⊢ hJ.dpow n (f a) = f (hI.dpow n a)
Theorem: DividedPowers.isDPMorphism_on_span
Proof state before:
A : Type u_1
B : Type u_2
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
S : Set A
hS : I = Ideal.span S
hS' : ∀ s ∈ S, f s ∈ J
hdp : ∀ (n : ℕ), ∀ a ∈ S, f (hI.dpow n a) = hJ.dpow n (f a)
h : Ideal.map f I ≤ J
dp_f : hI.dpMorphism hJ := hI.dpMorphismFromGens hJ hS h hdp
n : ℕ
a : A
ha : a ∈ I
⊢ hJ.dpow n (f a) = f (hI.dpow n a)
Tactic:
rw [← dpMorphismFromGens_coe hI hJ hS h hdp, dp_f.dpow_comp n a ha]
Proof state after:
no goals
Theorem: DividedPowers.isDPMorphism.of_comp
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
⊢ hI.isDPMorphism hJ f → hI.isDPMorphism hK h → hJ.isDPMorphism hK g
Tactic:
intro hf hh
Proof state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ hJ.isDPMorphism hK g
Theorem: DividedPowers.isDPMorphism.of_comp
Proof state before:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ hJ.isDPMorphism hK g
Tactic:
apply isDPMorphism_on_span
Proof state after:
case hS
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ J = Ideal.span ?S

case hS'
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ s ∈ ?S, g s ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ?S, g (hJ.dpow n a) = hK.dpow n (g a)

case S
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ Set B
Theorem: DividedPowers.isDPMorphism.of_comp
Proof state before:
case hS
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ J = Ideal.span ?S

case hS'
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ s ∈ ?S, g s ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ?S, g (hJ.dpow n a) = hK.dpow n (g a)

case S
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ Set B
Tactic:
exact sf
Proof state after:
case hS'
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ s ∈ ⇑f '' ↑I, g s ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Theorem: DividedPowers.isDPMorphism.of_comp
Proof state before:
case hS'
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ s ∈ ⇑f '' ↑I, g s ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
rintro b ⟨a, ha, rfl⟩
Proof state after:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ g (f a) ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Theorem: DividedPowers.isDPMorphism.of_comp
Proof state before:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ g (f a) ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)
Tactic:
rw [← RingHom.comp_apply]
Proof state after:
case hS'.intro.intro
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
a : A
ha : a ∈ ↑I
⊢ (g.comp f) a ∈ K

case hdp
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
h : A →+* C
hcomp : g.comp f = h
sf : J = Ideal.map f I
hf : hI.isDPMorphism hJ f
hh : hI.isDPMorphism hK h
⊢ ∀ (n : ℕ), ∀ a ∈ ⇑f '' ↑I, g (hJ.dpow n a) = hK.dpow n (g a)