Theorem: DividedPowers.isDPMorphism_on_span (DividedPowers/DPMorphism.lean)

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]
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

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]
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

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⟩
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

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
State after:
no goals

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
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)

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
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)

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
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)

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]
State after:
no goals