-- Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean
/-- If `B` is a faithfully flat `A`-algebra, the preimage of the pushforward of any
ideal `I` is again `I`. -/
lemma Ideal.comap_map_eq_self_of_faithfullyFlat (I : Ideal A) :
    (I.map (algebraMap A B)).comap (algebraMap A B) = I

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ comap (algebraMap A B) (map (algebraMap A B) I) ≤ I

Tactic:
have inj : Function.Injective
    ((quotIdealMapEquivTensorQuot B I).symm.toLinearMap.restrictScalars _ ∘ₗ
      TensorProduct.mk A B (A ⧸ I) 1) := by
  rw [LinearMap.coe_comp]
  exact (AlgEquiv.injective _).comp <|
    Module.FaithfullyFlat.tensorProduct_mk_injective (A ⧸ I)

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
⊢ comap (algebraMap A B) (map (algebraMap A B) I) ≤ I

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (Quotient.mk (map (algebraMap A B) I)) ((algebraMap A B) x) = 0
⊢ (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) ((Quotient.mk I) x) = 0

Tactic:
simp [← Algebra.algebraMap_eq_smul_one, hx]

Result:
no goals

Proof state:
case a
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (Quotient.mk (map (algebraMap A B) I)) ((algebraMap A B) x) = 0
⊢ (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) ((Quotient.mk I) x) =
    (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) 0

Tactic:
have : ((quotIdealMapEquivTensorQuot B I).symm.toLinearMap.restrictScalars _ ∘ₗ
    TensorProduct.mk A B (A ⧸ I) 1) x = 0 := by
  simp [← Algebra.algebraMap_eq_smul_one, hx]

Result:
case a
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (Quotient.mk (map (algebraMap A B) I)) ((algebraMap A B) x) = 0
this :
  (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) ((Quotient.mk I) x) = 0
⊢ (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) ((Quotient.mk I) x) =
    (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) 0

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : x ∈ comap (algebraMap A B) (map (algebraMap A B) I)
⊢ x ∈ I

Tactic:
rw [Ideal.mem_comap] at hx

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (algebraMap A B) x ∈ map (algebraMap A B) I
⊢ x ∈ I

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
⊢ comap (algebraMap A B) (map (algebraMap A B) I) ≤ I

Tactic:
intro x hx

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : x ∈ comap (algebraMap A B) (map (algebraMap A B) I)
⊢ x ∈ I

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)

Tactic:
rw [LinearMap.coe_comp]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ Function.Injective (⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap) ∘ ⇑((TensorProduct.mk A B (A ⧸ I)) 1))

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (algebraMap A B) x ∈ map (algebraMap A B) I
⊢ x ∈ I

Tactic:
rw [← Ideal.Quotient.eq_zero_iff_mem] at hx ⊢

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (Quotient.mk (map (algebraMap A B) I)) ((algebraMap A B) x) = 0
⊢ (Quotient.mk I) x = 0

Proof state:
case a
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
inj : Function.Injective ⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1)
x : A
hx : (Quotient.mk (map (algebraMap A B) I)) ((algebraMap A B) x) = 0
this :
  (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) ((Quotient.mk I) x) = 0
⊢ (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) ((Quotient.mk I) x) =
    (↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap ∘ₗ (TensorProduct.mk A B (A ⧸ I)) 1) 0

Tactic:
simp [this]

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ comap (algebraMap A B) (map (algebraMap A B) I) = I

Tactic:
refine le_antisymm ?_ le_comap_map

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ comap (algebraMap A B) (map (algebraMap A B) I) ≤ I

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Module.FaithfullyFlat A B
I : Ideal A
⊢ Function.Injective (⇑(↑A (quotIdealMapEquivTensorQuot B I).symm.toLinearMap) ∘ ⇑((TensorProduct.mk A B (A ⧸ I)) 1))

Tactic:
exact (AlgEquiv.injective _).comp <|
  Module.FaithfullyFlat.tensorProduct_mk_injective (A ⧸ I)

Result:
no goals