RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation.lean

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section structureMaps
variable (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel s t T))
include hequiv

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section structureMaps
variable (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel s t T))
include hequiv

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section structureMaps
variable (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel s t T))
include hequiv

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section structureMaps
variable (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel s t T))
include hequiv

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section shear
open CommRingCat
variable (hgen : s.range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel s t T))
  {P : Type u} [CommRing P] {inl inr c : B →+* P}
  (hP : IsPushout (ofHom t) (ofHom s) (ofHom inl) (ofHom inr))
  (hcs : c.comp s = inl.comp s) (hct : c.comp t = inr.comp t)
include hgen hequiv hP hcs hct

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section models
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] (t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section theta
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
include hequiv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section theta
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
include hgen hequiv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section rank
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section rank
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section rank
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
include hgen hequiv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section rank
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section rank
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
include hgen hequiv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section const
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B} [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
omit [Module.Finite A B] [Module.Projective A B] in
include hinj hinv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section const
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B} [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
include hgen hequiv hinj hinv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section const
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B} [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
include hgen hequiv hinj hinv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section envelope
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
variable {R S} (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section baseChange
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)
  (R' : Type u) [CommRing R'] [Algebra R R']

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section baseChange
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)
  (R' : Type u) [CommRing R'] [Algebra R R']

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section baseChange
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)
  (R' : Type u) [CommRing R'] [Algebra R R']

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section baseChange
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)
  (R' : Type u) [CommRing R'] [Algebra R R']

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section baseChange
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)
  (R' : Type u) [CommRing R'] [Algebra R R']

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section baseChange
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)
  (R' : Type u) [CommRing R'] [Algebra R R']

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section baseChange
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)
  (R' : Type u) [CommRing R'] [Algebra R R']

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section mapEquiv
variable {R S S₂ : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing S₂] [Algebra R S₂]
  (𝓔 : Envelope R S) (σ : S ≃ₐ[R] S₂)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section mapEquiv
variable {R S S₂ : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing S₂] [Algebra R S₂]
  (𝓔 : Envelope R S) (σ : S ≃ₐ[R] S₂)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section mapEquiv
variable {R S S₂ : Type u} [CommRing R] [CommRing S] [Algebra R S] [CommRing S₂] [Algebra R S₂]
  (𝓔 : Envelope R S) (σ : S ≃ₐ[R] S₂)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section split
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] (𝓔 : Envelope R S)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section localize
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S] (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)
  (𝓔 : Envelope R S) (J : Ideal R) [J.IsPrime]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section localize
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S] (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)
  (𝓔 : Envelope R S) (J : Ideal R) [J.IsPrime]
include hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section localize
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S] (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)
  (𝓔 : Envelope R S) (J : Ideal R) [J.IsPrime]
omit [Module.Finite R S] [Module.Projective R S] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section localize
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S] (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)
  (𝓔 : Envelope R S) (J : Ideal R) [J.IsPrime]
include hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1
section localize
variable {R S : Type u} [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S] (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)
  (𝓔 : Envelope R S) (J : Ideal R) [J.IsPrime]
include hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L1

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)
include hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)
include hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L1
variable (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] [Module.Finite R S]
  [Module.Projective R S]
open L1
variable (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := R) S p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L2
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L2
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L2
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L2
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
omit [Module.Finite A B] [Module.Projective A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L2
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
include hgen hequiv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L2
variable {A B : Type u} [CommRing A] [CommRing B] [Algebra A B] {t : A →+* B}
  [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
include hgen hequiv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L3
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra C A] (s t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L3
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra C A] (s t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L3
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra C A] (s t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L3
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra C A] (s t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L3
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra C A] (s t : A →+* B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))
omit [Algebra C A] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))
omit [Algebra C A] in
include hx in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))
omit [Algebra C A] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))
omit [Algebra C A] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))
include hequiv in
omit [Algebra C A] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))
include hequiv hinj hinv hx in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L6
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  {r : ℕ} (x : Fin r → A)
  (hx : Function.Bijective fun a : Fin r → A => ∑ i, algebraMap A B (a i) * t (x i))
include hequiv hinj hinv hx in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L8
variable (R : Type u) [CommRing R] [IsLocalRing R]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L8
variable (R : Type u) [CommRing R] [IsLocalRing R]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L8
variable (R : Type u) [CommRing R] [IsLocalRing R]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L8
variable (R : Type u) [CommRing R] [IsLocalRing R]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L8
variable (R : Type u) [CommRing R] [IsLocalRing R]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L8
variable (R : Type u) [CommRing R] [IsLocalRing R]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
open scoped L8 in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)
attribute [local instance] Algebra.TensorProduct.rightAlgebra in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)
attribute [local instance] Algebra.TensorProduct.rightAlgebra in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)
attribute [local instance] Algebra.TensorProduct.rightAlgebra in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)
attribute [local instance] Algebra.TensorProduct.rightAlgebra in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section generic
variable {C A B : Type u} [CommRing C] [CommRing A] [CommRing B] [Algebra C A] [Algebra C B]
  (C' : Type u) [CommRing C'] [Algebra C C'] (u : A →+* B)
  (hu : u.comp (algebraMap C A) = algebraMap C B)
attribute [local instance] Algebra.TensorProduct.rightAlgebra in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section lift
variable {C : Type u} [CommRing C] (C' : Type u) [CommRing C'] [Algebra C C']
  {X : Type u} [CommRing X] [Algebra C X] {T : Type u} [CommRing T]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section lift
variable {C : Type u} [CommRing C] (C' : Type u) [CommRing C'] [Algebra C C']
  {X : Type u} [CommRing X] [Algebra C X] {T : Type u} [CommRing T]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
namespace L7
section lift
variable {C : Type u} [CommRing C] (C' : Type u) [CommRing C'] [Algebra C C']
  {X : Type u} [CommRing X] [Algebra C X] {T : Type u} [CommRing T]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [Algebra C B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
attribute [local instance] Algebra.TensorProduct.rightAlgebra in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [Algebra C B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in
omit [Algebra A B] [Algebra C B] [IsScalarTower C A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
variable {A B : Type u} [CommRing A] [CommRing B] (s t : A →+* B)
variable {s t}
section L7
open L7
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B]
  (t : A →+* B) (C' : Type u) [CommRing C'] [Algebra C C']
variable {t} in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section antipode
variable (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
include hgen hequiv in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section antipode
variable (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section antipode
variable (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section norm
open L1
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section norm
open L1
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section norm
open L1
omit [Algebra A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section L4b
variable [Module.Finite A B] [Module.Projective A B]
  [Module.Finite A (Tgt t)] [Module.Projective A (Tgt t)]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
include hgen hequiv hinv hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L4
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section L4b
variable [Module.Finite A B] [Module.Projective A B]
  [Module.Finite A (Tgt t)] [Module.Projective A (Tgt t)]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
include hgen hequiv hinv hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section fibre
variable (t) (𝔪 : Ideal A)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section fibre
variable (t) (𝔪 : Ideal A)
omit [Algebra C A] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section fibre
variable (t) (𝔪 : Ideal A)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section fibre
variable (t) (𝔪 : Ideal A)

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section fibre
variable (t) (𝔪 : Ideal A)
variable (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section fibre
variable (t) (𝔪 : Ideal A)
variable (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section fibre
variable (t) (𝔪 : Ideal A)
variable (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
variable [Module.Finite A B] [Module.Projective A B] (r : ℕ)
  (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
include hr in
omit [Algebra C A] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section select
variable [IsLocalRing C] [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
omit [IsLocalRing C] [Module.Finite A B] [Module.Projective A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section select
variable [IsLocalRing C] [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
omit [IsLocalRing C] [Module.Finite A B] [Module.Projective A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section select
variable [IsLocalRing C] [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
omit [Module.Finite A B] [Module.Projective A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section select
variable [IsLocalRing C] [Module.Finite A B] [Module.Projective A B]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
include hgen hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section heart
variable [IsLocalRing C] [Module.Finite A B] [Module.Projective A B]
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
omit [IsLocalRing C] [Module.Projective A B] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section heart
variable [IsLocalRing C] [Module.Finite A B] [Module.Projective A B]
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
omit [IsLocalRing C] [Algebra C A] in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section L5
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  {t : A →+* B}
section heart
variable [IsLocalRing C] [Module.Finite A B] [Module.Projective A B]
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
variable [Module.Finite A (Tgt t)] [Module.Projective A (Tgt t)]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (r : ℕ) (hr : ∀ p, Module.rankAtStalk (R := A) B p = r)
include hgen hequiv hinv hr in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section theta
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] (t : A →+* B)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section theta
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] (t : A →+* B)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section theta
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] (t : A →+* B)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section theta
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] (t : A →+* B)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section theta
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] (t : A →+* B)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section descent
variable {C : Type u} [CommRing C]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section descent
variable {C : Type u} [CommRing C]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section descent
variable {C : Type u} [CommRing C]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section descent
variable {C : Type u} [CommRing C]

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section assembly
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] (t : A →+* B)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section assembly
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] (t : A →+* B)
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section localPackage
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] {t : A →+* B}

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section localPackage
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] {t : A →+* B}
variable [Module.Finite A B] [Module.Projective A B]
  [Module.Finite A (Tgt t)] [Module.Projective A (Tgt t)]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
include hgen hequiv hinj in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
namespace QuotFLF
section localPackage
variable {A B C : Type u} [CommRing A] [CommRing B] [CommRing C] [Algebra A B] [Algebra C A]
  [Algebra C B] [IsScalarTower C A B] {t : A →+* B}
variable [Module.Finite A B] [Module.Projective A B]
  [Module.Finite A (Tgt t)] [Module.Projective A (Tgt t)]
  (hgen : (algebraMap A B).range ⊔ t.range = ⊤)
  (hequiv : ∀ (T : Type u) [CommRing T], _root_.Equivalence (Rel (algebraMap A B) t T))
  (hinj : Function.Injective (algebraMap C A))
  (hinv : ∀ a : A, algebraMap A B a = t a ↔ a ∈ Set.range (algebraMap C A))
include hgen hequiv hinj in

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace RingHom_isPushout_eqLocus_of_finiteLocallyFree_equivalenceRelation
open CategoryTheory TensorProduct Polynomial
universe u
open QuotFLF in